perm filename FR81.XGP[S81,JMC]1 blob
sn#581747 filedate 1981-04-23 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXI30/FONT#2=BAXB30/FONT#3=BAXS30/FONT#4=GRFX25/FONT#9=MS25
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ L1
␈↓ ↓H␈↓α␈↓ βεTable of Contents
␈↓ ↓H␈↓α␈↓ αλSection␈↓ ¬wPage
␈↓ ↓H␈↓1. Basic Research in Arti␈↓α␈↓βC␈↓α␈↓cial Intelligence
␈↓ ↓H␈↓␈↓ αhand Formal Reasoning␈↓ ε∃ 2
␈↓ ↓H␈↓␈↓ ↓h1.1 Summary of Accomplishments and
␈↓ ↓H␈↓␈↓ αhWork Completed.␈↓ ε∃ 2
␈↓ ↓H␈↓␈↓ ↓h1.2 Some Unsolved Representation
␈↓ ↓H␈↓␈↓ αhProblems␈↓ ε∃ 5
␈↓ ↓H␈↓␈↓ ↓h1.3 The ANALYST␈↓ ε∃ 5
␈↓ ↓H␈↓␈↓ ↓h1.4 Proposed Work␈↓ ε∃ 8
␈↓ ↓H␈↓␈↓ α_1.4.1 Formal Reasoning and Basic
␈↓ ↓H␈↓␈↓ αhArti␈↓α␈↓βC␈↓α␈↓cial Intelligence␈↓ ε∃ 8
␈↓ ↓H␈↓␈↓ α_1.4.2 Representations and Reasoning:
␈↓ ↓H␈↓␈↓ αhTheoretical Foundations␈↓ ε∃ 9
␈↓ ↓H␈↓␈↓ α_1.4.3 An Advice-Taking ANALYST
␈↓ ↓H␈↓␈↓ αhProgram␈↓ εε 10
␈↓ ↓H␈↓␈↓ α_1.4.4 Architecture for Reasoning
␈↓ ↓H␈↓␈↓ αhPrograms␈↓ εε 15
␈↓ ↓H␈↓␈↓ α_1.4.5 Formalization of Mathematical
␈↓ ↓H␈↓␈↓ αhReasoning␈↓ εε 15
␈↓ ↓H␈↓␈↓ α_1.4.6 Formal Systems for
␈↓ ↓H␈↓␈↓ αhComputation Theories␈↓ εε 16
␈↓ ↓H␈↓␈↓ ↓h1.5 The Formal Reasoning Group␈↓ εε 19
␈↓ ↓H␈↓␈↓ ↓h1.6 References␈↓ εε 19
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ :2
␈↓ ↓H␈↓␈↓ ε Proposed
␈↓ ↓H␈↓α␈↓ ¬dBasic Research
␈↓ ↓H␈↓␈↓ ε;in
␈↓ ↓H␈↓α␈↓ ¬=Arti␈↓␈↓βc␈↓␈↓αcal Intelligence
␈↓ ↓H␈↓␈↓ ε/and
␈↓ ↓H␈↓α␈↓ ¬LFormal Reasoning
␈↓ ↓H␈↓␈↓ ¬;Principal Investigator
␈↓ ↓H␈↓␈↓ ¬aJohn McCarthy
␈↓ ↓H␈↓α␈↓ J2
␈↓ ↓H␈↓α␈↓ ↓a1. Basic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence␈↓ εh␈↓make it easier and easier to prepare machine-
␈↓ ↓H␈↓ αg␈↓αand Formal Reasoning ␈↓ εh␈↓aided and machine-checkable proofs of
␈↓ εh␈↓mathematical results in general and the
␈↓ ↓H␈↓␈↓αPersonnel: ␈↓ John McCarthy, Lewis Creary, ␈↓ εh␈↓correctness of computer programs in particular.
␈↓ ↓H␈↓␈↓ α_Jon Doyle, Richard Gabriel,
␈↓ ↓H␈↓␈↓ α_Jussi Ketonen, Carolyn Talcott, ␈↓↓Student ␈↓ εh␈↓The work on conjectural reasoning has led to
␈↓ ↓H␈↓↓␈↓ α_Research Assistants:␈↓ Jitendra Malik, ␈↓ εh␈↓␈↓↓circumscription␈↓, a form of non-monotonic
␈↓ ↓H␈↓␈↓ α_Joe Weening ␈↓ εh␈↓reasoning described in [McCarthy 1980a].
␈↓ εh␈↓Other forms of non-monotonic reasoning have
␈↓ ↓H␈↓Applied research requires basic research to␈↓ εh␈↓been developed.
␈↓ ↓H␈↓replenish the stock of ideas on which its
␈↓ ↓H␈↓progress depends. ␈↓ εh␈↓Indeed the epistemological studies have reached
␈↓ εh␈↓a point where we can propose to make an
␈↓ ↓H␈↓The long range goals of our work in basic AI␈↓ εh␈↓experimental Advice Taker to implement the
␈↓ ↓H␈↓and formal reasoning are to make computers␈↓ εh␈↓``intelligence'' ANALYST mentioned in our
␈↓ ↓H␈↓carry out the reasoning required to solve ␈↓ εh␈↓1979 proposal as a potential long range
␈↓ ↓H␈↓problems. This has involved studying the facts␈↓ εh␈↓application.
␈↓ ↓H␈↓of the common sense world and appropriate
␈↓ ↓H␈↓methods of common sense reasoning - both ␈↓ εh␈↓Until now the main work of the Formal
␈↓ ↓H␈↓rigorous and conjectural. These facts and␈↓ εh␈↓Reasoning Group has been theoretical. We
␈↓ ↓H␈↓modes of reasoning constitute the ␈↓ εh␈↓plan to continue the theoretical work, but it has
␈↓ ↓H␈↓␈↓↓epistemological␈↓ (knowledge theoretic) aspect of␈↓ εh␈↓advanced to the point where a major
␈↓ ↓H␈↓the arti␈↓↓␈↓βC␈↓↓␈↓cial intelligence problem. We have␈↓ εh␈↓experimental program aimed at eventual
␈↓ ↓H␈↓studied it apart from ␈↓↓heuristic␈↓ (search and␈↓ εh␈↓applications is possible. We have decided to
␈↓ ↓H␈↓pattern matching) problems as much as ␈↓ εh␈↓implement a version of the Advice Taker
␈↓ ↓H␈↓possible. ␈↓ εh␈↓proposed by McCarthy in 1958 [McCarthy
␈↓ εh␈↓1959] concentrating on the ``intelligence''
␈↓ ↓H␈↓The need to study epistemological problems of␈↓ εh␈↓ANALYST mentioned in our previous
␈↓ ↓H␈↓AI apart from heuristics has recently been␈↓ εh␈↓proposal.
␈↓ ↓H␈↓recognized by many AI researchers. We can
␈↓ ↓H␈↓cite Allen Newell's not yet published ␈↓ εh␈↓The advances that make ANALYST a feasible
␈↓ ↓H␈↓presidential address to the AAAI on the ␈↓ εh␈↓project include McCarthy and Creary results on
␈↓ ↓H␈↓``logical level'' of programs as well as work by␈↓ εh␈↓formalizing mental qualities and results of
␈↓ ↓H␈↓McDermott at Yale and Robert Moore at SRI.␈↓ εh␈↓McCarthy, Doyle and others on non-monotonic
␈↓ εh␈↓reasoning. Besides our own results, we rely on
␈↓ ↓H␈↓Research in formalizing the facts of the ␈↓ εh␈↓work by others including Gabriel on
␈↓ ↓H␈↓common sense world for AI purposes began ␈↓ εh␈↓conjectural reasoning based on comparative
␈↓ ↓H␈↓with McCarthy's 1959 ``Programs with Common␈↓ εh␈↓description matching.
␈↓ ↓H␈↓Sense''. The much used situational calculus was
␈↓ ↓H␈↓proposed in [McCarthy and Hayes 1969]. In␈↓ εh␈↓α␈↓ εm1.1 Summary of Accomplishments and Work
␈↓ ↓H␈↓recent years attention has turned to formalizing␈↓ εh␈↓ λU␈↓αCompleted.
␈↓ ↓H␈↓facts about knowledge, belief and wants. The
␈↓ ↓H␈↓problem of formalizing partial information␈↓ εh␈↓John McCarthy has continued his work on
␈↓ ↓H␈↓about concurrent processes long been a major␈↓ εh␈↓epistemological problems of arti␈↓↓␈↓βC␈↓↓␈↓cial
␈↓ ↓H␈↓barrier to progress in AI. ␈↓ εh␈↓intelligence, especially non-monotonic reasoning
␈↓ εh␈↓and the representation of knowledge and belief
␈↓ ↓H␈↓The work on rigorous reasoning has led to ␈↓ εh␈↓in ␈↓↓␈↓βC␈↓↓␈↓rst order logic. [McCarthy 1980]
␈↓ ↓H␈↓interactive proof generating and proving ␈↓ εh␈↓summarizes the state of the work on non-
␈↓ ↓H␈↓programs including Weyhrauch's FOL and the␈↓ εh␈↓monotonic reasoning as of Winter 1980, and
␈↓ ↓H␈↓newer EKL of Ketonen. Continued advances ␈↓ εh␈↓[McCarthy 1979] summarizes the 1979 results
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ J3
␈↓ ↓H␈↓on representation of concepts and propositions.␈↓ εh␈↓(2) The combinatorics of how errors in E could
␈↓ ↓H␈↓Beyond these results, McCarthy has developed␈↓ εh␈↓␈↓ π(have led to P (incorrectly) being written.
␈↓ ↓H␈↓a more general form of circumscription suitable␈↓ εh␈↓(3) The type of program behaviour that the
␈↓ ↓H␈↓for automatically generating frame axioms.␈↓ εh␈↓␈↓ π(programmer will observe when testing, for
␈↓ εh␈↓␈↓ π(example the program's output, or a trace.
␈↓ ↓H␈↓ He has also continued his work on the␈↓ εh␈↓(4) The characterisitics of ``complete'' test data,
␈↓ ↓H␈↓Elephant formalism for representing programs.␈↓ εh␈↓␈↓ π(which is guaranteed to reveal the presence
␈↓ ↓H␈↓This permits entirely conventional programs to␈↓ εh␈↓␈↓ π(of errors in E, assuming all errors come
␈↓ ↓H␈↓be regarded as sentences of logic from which␈↓ εh␈↓␈↓ π(from E.
␈↓ ↓H␈↓their properties follow without any special logic
␈↓ ↓H␈↓of programming. This involves representing␈↓ εh␈↓The theory is developed at a general level and
␈↓ ↓H␈↓variables including the program counter ␈↓ εh␈↓is then specialized to the case of recursive
␈↓ ↓H␈↓explicitly as functions of time and has led to␈↓ εh␈↓programs having only simple errors, where the
␈↓ ↓H␈↓controversy with the advocates of temporal␈↓ εh␈↓programmer observes a trace of each test run.
␈↓ ↓H␈↓logic. Elephant also allows explicit reference to␈↓ εh␈↓A method is devised for generating test data,
␈↓ ↓H␈↓past events and actions without having to ␈↓ εh␈↓based on this application of the theory. The
␈↓ ↓H␈↓declare variables or arrays to represent the␈↓ εh␈↓generated test data is ``complete'', meaning that
␈↓ ↓H␈↓information that has to be remembered by the␈↓ εh␈↓if the only errors in the recursive program are
␈↓ ↓H␈↓program. This makes it a higher level ␈↓ εh␈↓of the speci␈↓↓␈↓βC␈↓↓␈↓ed types, then the test data will
␈↓ ↓H␈↓language than almost all present languages, but␈↓ εh␈↓reveal the errors through at least one incorrect
␈↓ ↓H␈↓it is not yet clear how to take best advantage of␈↓ εh␈↓trace.
␈↓ ↓H␈↓this fact. Results on Elephant will be published
␈↓ ↓H␈↓shortly [McCarthy 1981]. ␈↓ εh␈↓Viewed contrapositively, assuming that the
␈↓ εh␈↓written program P is ``almost correct'', that is,
␈↓ ↓H␈↓Luigia Aiello did extensive work demonstrating␈↓ εh␈↓di␈↓↓␈↓β@␈↓↓␈↓ers from the correct program at most by
␈↓ ↓H␈↓how metatheory can be used to represent ␈↓ εh␈↓errors of the speci␈↓↓␈↓βC␈↓↓␈↓ed simple types E, if the
␈↓ ↓H␈↓elementary algebra in a reasonable way. She␈↓ εh␈↓trace of each test run is as the programmer
␈↓ ↓H␈↓wrote an algebraic simpli␈↓↓␈↓βC␈↓↓␈↓er that used meta␈↓ εh␈↓intended, then the program must be correct.
␈↓ ↓H␈↓reasoning to make decisions about which ␈↓ εh␈↓The test data generation method has been
␈↓ ↓H␈↓simpli␈↓↓␈↓βC␈↓↓␈↓cations should be used [Aiello and ␈↓ εh␈↓implemented (in MacLisp) and examples of its
␈↓ ↓H␈↓Weyhrauch 1980]. She also wrote a `compiler'␈↓ εh␈↓operation are given.
␈↓ ↓H␈↓for converting e␈↓↓␈↓β@␈↓↓␈↓ective axiomatic descriptions
␈↓ ↓H␈↓of functions (as part of a theory) into programs␈↓ εh␈↓Lewis Creary's research during the past year
␈↓ ↓H␈↓(the interpretation in the intended model)␈↓ εh␈↓has concentrated on epistemological and
␈↓ ↓H␈↓[Aiello 1980]. The work was carried out using␈↓ εh␈↓representational problems of commonsense
␈↓ ↓H␈↓FOL [Weyhrauch 1977,1979]. She used and ␈↓ εh␈↓reasoning, and of causal reasoning in
␈↓ ↓H␈↓extended technology developed by [Talcott and␈↓ εh␈↓particular. He has constructed a general
␈↓ ↓H␈↓Weyhrach 1981] for exploiting the theory- ␈↓ εh␈↓epistemological framework for the study of
␈↓ ↓H␈↓metatheory and theory-model connections that␈↓ εh␈↓commonsense factual reasoning that is
␈↓ ↓H␈↓are basic to the FOL formalism. ␈↓ εh␈↓speci␈↓↓␈↓βC␈↓↓␈↓cally oriented to the needs of research in
␈↓ εh␈↓arti␈↓↓␈↓βC␈↓↓␈↓cial intelligence. The framework, which is
␈↓ ↓H␈↓Martin Brooks completed his thesis which ␈↓ εh␈↓presented in [Creary 1981b], incorporates a
␈↓ ↓H␈↓describes how testing can be used to show a␈↓ εh␈↓``competing considerations'' model of factual
␈↓ ↓H␈↓program's correctness.[Brooks 1980] The ␈↓ εh␈↓reasoning, according to which such reasoning
␈↓ ↓H␈↓scenario for using testing to show correctness is␈↓ εh␈↓involves the weighing and composition of all
␈↓ ↓H␈↓that the programmer writes a program P which␈↓ εh␈↓reasonably discoverable considerations bearing
␈↓ ↓H␈↓is either correct, or which di␈↓↓␈↓β@␈↓↓␈↓ers from the␈↓ εh␈↓on a set of target propositions. While the work
␈↓ ↓H␈↓correct program by one or more errors in a␈↓ εh␈↓on causal reasoning is not yet ␈↓↓␈↓βC␈↓↓␈↓nished, it has
␈↓ ↓H␈↓speci␈↓↓␈↓βC␈↓↓␈↓ed class E of errors. The theory relates:␈↓ εh␈↓yielded as a byproduct a philosophical paper
␈↓ ↓H␈↓(1) P's structure. ␈↓ εh␈↓[Creary 1981a] on the need to take forces and
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ G4
␈↓ ↓H␈↓related causal in␈↓↓␈↓βD␈↓↓␈↓uences seriously in the ␈↓ εh␈↓The notation provides a complement to tabular
␈↓ ↓H␈↓analysis of causal explanation. ␈↓ εh␈↓analysis and computer simulation for
␈↓ εh␈↓manipulating and checking digital devices and
␈↓ ↓H␈↓Chris Goad has completed a thesis ␈↓ εh␈↓has the advantage that it corresponds closely
␈↓ ↓H␈↓concerning the manipulation of algorithms␈↓ εh␈↓with the intuitive notions of circuit principles.
␈↓ ↓H␈↓expressed by formal proofs [Goad 1980a,b]. A␈↓ εh␈↓In addition, it readily permits incomplete
␈↓ ↓H␈↓brief description of his thesis work follows.␈↓ εh␈↓speci␈↓↓␈↓βC␈↓↓␈↓cations of devices and allows for formal
␈↓ εh␈↓proofs. The formalism naturally includes the
␈↓ ↓H␈↓As has been known since the 1940's, a proof of␈↓ εh␈↓ability to hierarchically structure behavior and
␈↓ ↓H␈↓a proposition of the form `for all x there exists␈↓ εh␈↓proofs so that the internal details of a
␈↓ ↓H␈↓some y such that the relation R holds between␈↓ εh␈↓component can be ignored once desired
␈↓ ↓H␈↓x and y' can, under the right conditions, serve␈↓ εh␈↓properties have been substantiated.
␈↓ ↓H␈↓as a `program' for computing values for y from
␈↓ ↓H␈↓values for x. Such a proof describes a␈↓ εh␈↓Carolyn Talcott has completed the main work
␈↓ ↓H␈↓method of computation - an algorithm - in a␈↓ εh␈↓on the FOLISP project. This work involved
␈↓ ↓H␈↓way which is rather di␈↓↓␈↓β@␈↓↓␈↓erent from the way in␈↓ εh␈↓expressing the ideas of [McCarthy and
␈↓ ↓H␈↓which the same algorithm would be ␈↓ εh␈↓Cartwright 1979] for representation of LISP
␈↓ ↓H␈↓described by a conventional program. For␈↓ εh␈↓Program in ␈↓↓␈↓βC␈↓↓␈↓rst order logic in the FOL
␈↓ ↓H␈↓one thing, a proof contains information about␈↓ εh␈↓formalism [Weyhrauch 1977]. Proofs of a
␈↓ ↓H␈↓an algorithm which is not present in the␈↓ εh␈↓variety of properties of LISP programs were
␈↓ ↓H␈↓corresponding program. Goad's thesis showed␈↓ εh␈↓written and checked by FOL. They included
␈↓ ↓H␈↓that the di␈↓↓␈↓β@␈↓↓␈↓erences between proofs and ␈↓ εh␈↓all the examples discussed in ``LISP:
␈↓ ↓H␈↓ordinary programs can be exploited in the ␈↓ εh␈↓Programming and Proving'' [McCarthy and
␈↓ ↓H␈↓automatic specialization and optimization of␈↓ εh␈↓Talcott 1981, Chapters III and IV].
␈↓ ↓H␈↓algorithms. Goad worked out one non-trivial
␈↓ ↓H␈↓and fully concrete application, namely, the use␈↓ εh␈↓Among the techniques illustrated are:
␈↓ ↓H␈↓of proof transformations familiar from proof␈↓ εh␈↓␈↓ πλ1. representation of recursive programs,
␈↓ ↓H␈↓theory in the automatic specialization of a␈↓ εh␈↓␈↓ πλ2. use of structural and rank induction to
␈↓ ↓H␈↓bin-packing algorithm which was formally ␈↓ εh␈↓␈↓ π8prove properties of total recursive
␈↓ ↓H␈↓described by a proof. The application was␈↓ εh␈↓␈↓ π8functions,
␈↓ ↓H␈↓carried out by use of a proof manipulation␈↓ εh␈↓␈↓ πλ3. use of McCarthy's minimization schema to
␈↓ ↓H␈↓system developed by Goad on the Stanford␈↓ εh␈↓␈↓ π8prove properties of partial recursive
␈↓ ↓H␈↓Arti␈↓↓␈↓βC␈↓↓␈↓cial Intelligence Laboratory PDP-10 ␈↓ εh␈↓␈↓ π8functions,
␈↓ ↓H␈↓computer. The application was successful in␈↓ εh␈↓␈↓ πλ4. representation of iterative programs using
␈↓ ↓H␈↓the sense that substantial gains in ␈↓ εh␈↓␈↓ π8the Elephant formalism [McCarthy 1980],
␈↓ ↓H␈↓e␈↓↓␈↓β@␈↓↓␈↓iciency were produced by proof ␈↓ εh␈↓␈↓ π8and
␈↓ ↓H␈↓transformations which have no analogs among␈↓ εh␈↓␈↓ πλ5. use of the method of intermittent
␈↓ ↓H␈↓the transformations applicable to ordinary␈↓ εh␈↓␈↓ π8assertions [Manna and Waldinger 1978]
␈↓ ↓H␈↓programs. ␈↓ εh␈↓␈↓ π8to prove properties of iterative programs
␈↓ εh␈↓␈↓ π8represented in the Elephant formalism.
␈↓ ↓H␈↓Ben Moszkowski has been investigating how to
␈↓ ↓H␈↓model digital circuits using temporal logic and␈↓ εh␈↓In addition the FOLISP system in FOL was
␈↓ ↓H␈↓denotational semantics. The goal is to ␈↓ εh␈↓developed su␈↓↓␈↓β@␈↓↓␈↓iciently to be useable by students
␈↓ ↓H␈↓naturally, yet rigorously describe and reason␈↓ εh␈↓in the advanced theory of computation course
␈↓ ↓H␈↓about signal propagation, asynchronous ␈↓ εh␈↓for representing and checking their own proofs.
␈↓ ↓H␈↓operation, feedback and general input/output␈↓ εh␈↓A description of this work is contained in
␈↓ ↓H␈↓aspects of digital components. His methodology␈↓ εh␈↓[Talcott 1981].
␈↓ ↓H␈↓provides the means for proving proper
␈↓ ↓H␈↓behavior in actual circuits in a manner similar␈↓ εh␈↓Ma Xiwen revised McCarthy's set of axioms
␈↓ ↓H␈↓to that for higher level program veri␈↓↓␈↓βC␈↓↓␈↓cation.␈↓ εh␈↓for representing the rather di␈↓↓␈↓β@␈↓↓␈↓icult knowledge
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ I5
␈↓ ↓H␈↓puzzle of Mr. S and Mr. P and used FOL to ␈↓ εh␈↓Facts of these kinds cannot be adequately
␈↓ ↓H␈↓verify the translation of the knowledge problem␈↓ εh␈↓represented in data bases at present, and there
␈↓ ↓H␈↓to a purely arithmetic problem. This work is␈↓ εh␈↓are undoubtedly other phenomena essential for
␈↓ ↓H␈↓part of a study of the representation of facts␈↓ εh␈↓intelligence which have yet to be discovered.
␈↓ ↓H␈↓about knowledge that will aid the development␈↓ εh␈↓Before such facts can be incorporated in data
␈↓ ↓H␈↓of programs that know what people and other␈↓ εh␈↓bases and question-answering programs in a
␈↓ ↓H␈↓programs do and don't know. ␈↓ εh␈↓general way, basic research must determine the
␈↓ εh␈↓logical structure of these concepts.
␈↓ ↓H␈↓The following students completed their thesis
␈↓ ↓H␈↓work: Juan Bulnes [Bulnes-Rozas 1979] and ␈↓ εh␈↓Before discussing our planned work on these
␈↓ ↓H␈↓David Wilkins [Wilkins 1979]. ␈↓ εh␈↓epistemological problems technically, we discuss
␈↓ εh␈↓an experimental application that we are now in
␈↓ ↓H␈↓α␈↓ ↓R1.2 Some Unsolved Representation Problems␈↓ εh␈↓a position to undertake.
␈↓ ↓H␈↓Although much of our work is technical and␈↓ εh␈↓α␈↓ λ≥1.3 The ANALYST
␈↓ ↓H␈↓abstract, the results will have important
␈↓ ↓H␈↓practical applications. Also, consideration of␈↓ εh␈↓ANALYST scans a computerized ``intelligence''
␈↓ ↓H␈↓solutions to practical problems helps to isolate␈↓ εh␈↓data base. It looks for patterns of information
␈↓ ↓H␈↓and clarify some of the technical issues. For␈↓ εh␈↓that suggest conjectures about an adversary's
␈↓ ↓H␈↓example, consider the problem of designing and␈↓ εh␈↓capabilities, intentions, knowledge, beliefs and
␈↓ ↓H␈↓e␈↓↓␈↓β@␈↓↓␈↓ectively using data bases. For data bases to␈↓ εh␈↓goals. When ANALYST thinks it has found
␈↓ ↓H␈↓include many types of information that decision␈↓ εh␈↓something signi␈↓↓␈↓βC␈↓↓␈↓cant, it informs a human
␈↓ ↓H␈↓makers really need will require major advances␈↓ εh␈↓analyst about its conclusions (and if requested
␈↓ ↓H␈↓in representation theory. Programs that use the␈↓ εh␈↓about how it reached them). Its forte is
␈↓ ↓H␈↓information e␈↓↓␈↓β@␈↓↓␈↓ectively impose requirements on␈↓ εh␈↓examining more data than is possible for a
␈↓ ↓H␈↓the representation and also need new modes of␈↓ εh␈↓human and guaranteeing that all possibilities of
␈↓ ↓H␈↓reasoning. Thus current data base technology␈↓ εh␈↓the kinds it is programmed for are pursued.
␈↓ ↓H␈↓at best allows simple relations to be represented␈↓ εh␈↓The example is somewhat contrived, because
␈↓ ↓H␈↓- e.g. ``Smith is the supervisor of Jones.''␈↓ εh␈↓we have emphasized the problems we are
␈↓ ↓H␈↓Additions from current AI techniques would␈↓ εh␈↓currently studying and ignored others.
␈↓ ↓H␈↓allow simple generalizations of relations (``Every␈↓ εh␈↓Moreover, the ANALYST we plan to program
␈↓ ↓H␈↓employee has a supervisor except the director.''),␈↓ εh␈↓will be quite limited in its capabilities, partly
␈↓ ↓H␈↓but this leaves a tremendous range of ␈↓ εh␈↓because we have only partially solved the
␈↓ ↓H␈↓representation problems untreated: ␈↓ εh␈↓problems we are studying, but mainly because
␈↓ εh␈↓of problems no-one has begun to study.
␈↓ ↓H␈↓␈↓ ↓h1. Mental states - what a person or group
␈↓ ↓H␈↓␈↓ α_believes, knows, wants, fears, etc. ␈↓ εh␈↓Suppose ANALYST reads in a report from
␈↓ ↓H␈↓␈↓ ↓h2. Modalities - what may happen, what must␈↓ εh␈↓Damascus:
␈↓ ↓H␈↓␈↓ α_happen, what ought to be done, what
␈↓ ↓H␈↓␈↓ α_can be done, etc. ␈↓ εh␈↓␈↓ πλ␈↓↓Major Alexei Ivanov went to Damascus
␈↓ ↓H␈↓␈↓ ↓h3. Conjectures - if something were true what␈↓ εh␈↓↓␈↓ πλairport, bought a ticket to Moscow for cash,
␈↓ ↓H␈↓␈↓ α_else would be the case. ␈↓ εh␈↓↓␈↓ πλand departed on the next ␈↓␈↓βT␈↓␈↓↓ight to Moscow␈↓.
␈↓ ↓H␈↓␈↓ ↓h4. Causality - how does one event follow
␈↓ ↓H␈↓␈↓ α_because of another. The preconditions of ␈↓ εh␈↓ANALYST asks itself why Ivanov did what he
␈↓ ↓H␈↓␈↓ α_events and the consequences of events. ␈↓ εh␈↓did. Usually it ␈↓↓␈↓βC␈↓↓␈↓nds hypotheses that ␈↓↓␈↓βC␈↓↓␈↓t a
␈↓ ↓H␈↓␈↓ α_concurrent events and their laws of ␈↓ εh␈↓normal pattern of behavior and gains nothing
␈↓ ↓H␈↓␈↓ α_interaction and non-interaction. ␈↓ εh␈↓but further de␈↓↓␈↓βC␈↓↓␈↓ning the normal pattern. Let's
␈↓ ↓H␈↓␈↓ ↓h5. Actions and their modi␈↓↓␈↓βC␈↓↓␈↓ers, e.g. ``slowly''.␈↓ εh␈↓suppose there is more in this case.
␈↓ ↓H␈↓␈↓ ↓h6. Ability - conditions under which a person
␈↓ ↓H␈↓␈↓ α_or group can do something. ␈↓ εh␈↓␈↓↓Why did he pay cash␈↓? This question arises
␈↓ ↓H␈↓␈↓ ↓h7. Obligation or owing.
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ J6
␈↓ ↓H␈↓from a program that looks for motives of ␈↓ εh␈↓α␈↓ πkRepresenting general facts
␈↓ ↓H␈↓actions that are found to deviate from a normal
␈↓ ↓H␈↓pattern. We suppose that the data base ␈↓ εh␈↓Few existing data base systems represent
␈↓ ↓H␈↓contains a statement that Russians usually buy␈↓ εh␈↓general facts by entries in the data base. For
␈↓ ↓H␈↓tickets from their travel agency Intourist. The␈↓ εh␈↓example, ANALYST needs to represent the
␈↓ ↓H␈↓conjecture is then formed that Ivanov is in a␈↓ εh␈↓fact that the Russians almost always buy their
␈↓ ↓H␈↓hurry and that some event has required him to␈↓ εh␈↓airline tickets from Intourist in such a way that
␈↓ ↓H␈↓go to Moscow suddenly. The hypothesis is ␈↓ εh␈↓further deductions can be made and the fact
␈↓ ↓H␈↓con␈↓↓␈↓βC␈↓↓␈↓rmed by discovering that he had ␈↓ εh␈↓can be modi␈↓↓␈↓βC␈↓↓␈↓ed by new evidence. Existing
␈↓ ↓H␈↓previously accepted an invitation incompatible␈↓ εh␈↓systems represent them by program or by ␈↓↓semi-
␈↓ ↓H␈↓with a Moscow trip. ␈↓ εh␈↓↓programs␈↓ like productions. This works very
␈↓ εh␈↓well for applying the general facts to particular
␈↓ ↓H␈↓Now suppose that it is known or conjectured␈↓ εh␈↓cases, but it doesn't work as well for deducing
␈↓ ↓H␈↓that Ivanov is a radar expert. This leads␈↓ εh␈↓new general facts from old ones or representing
␈↓ ↓H␈↓ANALYST to scan facts about our adversary ␈↓ εh␈↓facts about facts. In order to represent general
␈↓ ↓H␈↓relationship with the Russians in the ␈↓↓␈↓βC␈↓↓␈↓eld of␈↓ εh␈↓assertions, e.g. Russians buy their tickets from
␈↓ ↓H␈↓radar including the fact that we are trying to␈↓ εh␈↓Intourist, one needs quanti␈↓↓␈↓βC␈↓↓␈↓ers, and the most
␈↓ ↓H␈↓␈↓↓␈↓βC␈↓↓␈↓nd out the pattern of frequency variation of␈↓ εh␈↓developed logical system with quanti␈↓↓␈↓βC␈↓↓␈↓ers is ␈↓↓␈↓βC␈↓↓␈↓rst
␈↓ ↓H␈↓their radars. One general fact in the data base␈↓ εh␈↓order logic. Even within ␈↓↓␈↓βC␈↓↓␈↓rst order logic, there
␈↓ ↓H␈↓is that when one side ␈↓↓␈↓βC␈↓↓␈↓nds out the frequency␈↓ εh␈↓are many possible ways of representing a
␈↓ ↓H␈↓variation pattern of a radar, the other side␈↓ εh␈↓particular kind of fact, and much further study
␈↓ ↓H␈↓wants to change it. ␈↓↓Therefore, analyst ␈↓ εh␈↓is required.
␈↓ ↓H␈↓↓conjectures that the Russians think we will soon
␈↓ ↓H␈↓↓know the frequency variation pattern of their␈↓ εh␈↓α␈↓ λ∞Knowledge and belief
␈↓ ↓H␈↓↓R111 radar␈↓.
␈↓ εh␈↓The notion ␈↓↓X thinks Y will soon know Z␈↓ is not
␈↓ ↓H␈↓This simple example poses several problems not␈↓ εh␈↓unusually complex when adversaries try to
␈↓ ↓H␈↓handled by present database programs. First,␈↓ εh␈↓outwit each other. It presents problems for
␈↓ ↓H␈↓present data base systems store particular facts,␈↓ εh␈↓machine representation that haven't been
␈↓ ↓H␈↓not general facts. General facts usually have to␈↓ εh␈↓conclusively solved but on which we have made
␈↓ ↓H␈↓be built into programs or at least into ␈↓ εh␈↓recent progress.
␈↓ ↓H␈↓productions. Second, the laws that determine
␈↓ ↓H␈↓what conclusions can be drawn from facts ␈↓ εh␈↓In order to be useful ANALYST must do more
␈↓ ↓H␈↓about knowledge, belief and intentions are␈↓ εh␈↓than just represent the above fact. It must be
␈↓ ↓H␈↓di␈↓↓␈↓β@␈↓↓␈↓erent from those governing non-mental ␈↓ εh␈↓able to prove or conjecture it under appropriate
␈↓ ↓H␈↓qualities, and present programs don't use the␈↓ εh␈↓circumstances and it must be able to draw
␈↓ ↓H␈↓laws that apply to these ␈↓↓modal␈↓ concepts. Third,␈↓ εh␈↓correct conclusions from it - and not draw
␈↓ ↓H␈↓the reasoning required even to conjecture that␈↓ εh␈↓incorrect conclusions. The latter is the more
␈↓ ↓H␈↓Ivanov is in a hurry involves conjecturing that␈↓ εh␈↓immediate problem. Let us use a simpler
␈↓ ↓H␈↓his behavior is normal except in so far as␈↓ εh␈↓example. Suppose we have the sentences ␈↓↓Pat
␈↓ ↓H␈↓speci␈↓↓␈↓βC␈↓↓␈↓c facts suggest abnormalities. Fourth,␈↓ εh␈↓↓knows Mike's telephone number␈↓ and ␈↓↓Mike's
␈↓ ↓H␈↓many reasoning processes involve observation␈↓ εh␈↓↓telephone number is the same as Mary's␈↓. A
␈↓ ↓H␈↓as well as reasoning from facts in a data base.␈↓ εh␈↓computerized deduction system that uses the
␈↓ ↓H␈↓Obtaining the con␈↓↓␈↓βC␈↓↓␈↓rming evidence that Ivanov␈↓ εh␈↓rule that equals may be substituted for equals
␈↓ ↓H␈↓is in a hurry has that character. Finally, the␈↓ εh␈↓might conclude ␈↓↓Pat knows Mary's telephone
␈↓ ↓H␈↓pattern recognition required to conjecture from␈↓ εh␈↓↓number␈↓. This is not a legitimate deduction,
␈↓ ↓H␈↓Ivanov's hurried Moscow trip and the ␈↓ εh␈↓even though it would be legitimate to deduce
␈↓ ↓H␈↓previously known facts that they think we will␈↓ εh␈↓that Pat dialed Mary's telephone number from
␈↓ ↓H␈↓soon know their radar pattern is quite di␈↓↓␈↓β@␈↓↓␈↓erent␈↓ εh␈↓the fact that he dialed Mike's number and the
␈↓ ↓H␈↓from that done today. We shall consider these␈↓ εh␈↓fact that the numbers are the same.
␈↓ ↓H␈↓problems in turn.
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ J7
␈↓ ↓H␈↓The fact that substitution of equals for equals␈↓ εh␈↓situations, one has already considered or been
␈↓ ↓H␈↓is legitimate in some contexts and not in others␈↓ εh␈↓told what are the reasonable assumptions to
␈↓ ↓H␈↓has been well known for a very long time. ␈↓ εh␈↓make, and these can simply be stated as general,
␈↓ ↓H␈↓Correct logical laws for handling such cases␈↓ εh␈↓rule-of-thumb facts, that is, rules which tolerate
␈↓ ↓H␈↓have been proposed, but the presently known␈↓ εh␈↓exceptions. Partial solutions to both of these
␈↓ ↓H␈↓solutions have two defects. First they usually␈↓ εh␈↓problems have been found: to the ␈↓↓␈↓βC␈↓↓␈↓rst, a
␈↓ ↓H␈↓treat only one such function at a time such as␈↓ εh␈↓technique called circumscription [McCarthy
␈↓ ↓H␈↓``knows'' while real life problems often mix up␈↓ εh␈↓1980a], and to the second, techniques called
␈↓ ↓H␈↓several even in the same sentence, e.g. think␈↓ εh␈↓default rules and reason maintenance.
␈↓ ↓H␈↓and know - ␈↓↓They think we will soon know ...␈↓.
␈↓ ↓H␈↓Second, each such mental quality requires ␈↓ εh␈↓The problem of making routine assumptions
␈↓ ↓H␈↓modifying the logic. In a practical case this␈↓ εh␈↓has been approached in many ways in arti␈↓↓␈↓βC␈↓↓␈↓cial
␈↓ ↓H␈↓would be many months work and might have ␈↓ εh␈↓intelligence programs, perhaps the most
␈↓ ↓H␈↓to be done again and again. ␈↓ εh␈↓common being the technique of default ␈↓↓␈↓βC␈↓↓␈↓llers of
␈↓ εh␈↓frame slots. These techniques all had serious
␈↓ ↓H␈↓α␈↓ β1Conjectures ␈↓ εh␈↓problems, though, as they did not interpret the
␈↓ εh␈↓statements of these defaults carefully enough to
␈↓ ↓H␈↓It has long been recognized that standard logic␈↓ εh␈↓ensure sensible behavior. Recently Jon Doyle
␈↓ ↓H␈↓does not represent the many kinds of reasoning␈↓ εh␈↓proposed reason maintenance systems a ␈↓↓␈↓βC␈↓↓␈↓rst
␈↓ ↓H␈↓that people use in forming conjectures. It now␈↓ εh␈↓solution to this problem [Doyle 1979, 1980].
␈↓ ↓H␈↓appears that much human reasoning involves␈↓ εh␈↓Reason maintenance systems record the
␈↓ ↓H␈↓conjecturing that the known facts about a ␈↓ εh␈↓inferences made by a reasoner, and examine the
␈↓ ↓H␈↓phenomenon are all the relevant facts. Thus␈↓ εh␈↓set of reasons to decide on a coherent set of
␈↓ ↓H␈↓ANALYST must conjecture that Ivanov was in␈↓ εh␈↓assumptions to adopt. Routine assumptions
␈↓ ↓H␈↓a hurry because it has no other explanation␈↓ εh␈↓appear in this framework as default rules, such
␈↓ ↓H␈↓even though it cannot conclusively exclude␈↓ εh␈↓as ``All birds ␈↓↓␈↓βD␈↓↓␈↓y,'' which are used to construct
␈↓ ↓H␈↓other explanations. ␈↓ εh␈↓non-monotonic justi␈↓↓␈↓βC␈↓↓␈↓cations, records of non-
␈↓ εh␈↓monotonic inferences. In addition to their
␈↓ ↓H␈↓Strict logical deduction does not permit drawing␈↓ εh␈↓importance in making assumptions, reason
␈↓ ↓H␈↓a conclusion from certain facts that would be␈↓ εh␈↓maintenance systems are instrumental in many
␈↓ ↓H␈↓changed if additional facts, supplementing but␈↓ εh␈↓other necessary functions of reasoning
␈↓ ↓H␈↓not contradicting them, were discovered. In␈↓ εh␈↓programs, including database updates,
␈↓ ↓H␈↓logic, if a conclusion follows, it will still follow␈↓ εh␈↓explanation of database entries, and, as
␈↓ ↓H␈↓when more facts are added. Humans, on the␈↓ εh␈↓explained next, decision-making.
␈↓ ↓H␈↓other hand, are always drawing this kind of
␈↓ ↓H␈↓conclusion. We now think that machines must␈↓ εh␈↓α␈↓ λ.Decision-Making
␈↓ ↓H␈↓also reason this way, and that programs
␈↓ ↓H␈↓con␈↓↓␈↓βC␈↓↓␈↓ned to strict logical reasoning must either␈↓ εh␈↓A key problem for any agent carrying out
␈↓ ↓H␈↓be unable to draw conclusions or they must use␈↓ εh␈↓complex activities or solving di␈↓↓␈↓β@␈↓↓␈↓icult problems
␈↓ ↓H␈↓axioms so unquali␈↓↓␈↓βC␈↓↓␈↓ed that they are false. ␈↓ εh␈↓is that of making decisions. For example,
␈↓ εh␈↓ANALYST must make decisions about which
␈↓ ↓H␈↓There are two parts to the problem of drawing␈↓ εh␈↓possible interpretation to take of each new fact
␈↓ ↓H␈↓such tentative conclusions. The ␈↓↓␈↓βC␈↓↓␈↓rst part is that␈↓ εh␈↓learned, and must also make further decisions
␈↓ ↓H␈↓of deciding what assumptions to make to ␈↓ εh␈↓about how to ␈↓↓␈↓βC␈↓↓␈↓t these individual decisions into
␈↓ ↓H␈↓facilitate one's reasoning, and the second part is␈↓ εh␈↓global interpretations of what is going on.
␈↓ ↓H␈↓that of actually making those assumptions. The␈↓ εh␈↓Subjective Bayesian decision theory is perhaps
␈↓ ↓H␈↓␈↓↓␈↓βC␈↓↓␈↓rst of these problems is di␈↓↓␈↓β@␈↓↓␈↓icult in novel␈↓ εh␈↓the best developed formal theory of making
␈↓ ↓H␈↓situations, for one just knows one lacks ␈↓ εh␈↓decisions, but proves overly restrictive in its
␈↓ ↓H␈↓information, without being sure exactly what␈↓ εh␈↓requirement of complete information about
␈↓ ↓H␈↓one should know. However, in routine ␈↓ εh␈↓actions, consequences, and utilities. Recently
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ I8
␈↓ ↓H␈↓Jon Doyle has developed a new technique for␈↓ εh␈↓programs ␈↓↓␈↓βC␈↓↓␈↓nd patterns in observed data rather
␈↓ ↓H␈↓decision-making called reasoned deliberation␈↓ εh␈↓than introduce new entities in order to explain
␈↓ ↓H␈↓[Doyle 1980]. Reasoned deliberation views the␈↓ εh␈↓the data.
␈↓ ↓H␈↓decision-making process as a reasoning task
␈↓ ↓H␈↓itself. It involves incremental construction, by␈↓ εh␈↓α␈↓ λ≥1.4 Proposed Work
␈↓ ↓H␈↓means of general rules of thumb about
␈↓ ↓H␈↓decision-making, of the various possible ␈↓ εh␈↓Now we present in more detail the technical
␈↓ ↓H␈↓actions, their expected consequences, and the␈↓ εh␈↓aspects of our planned work.
␈↓ ↓H␈↓partial preferences and utilites (when known)
␈↓ ↓H␈↓among them. It applies these general rules in a␈↓ εh␈↓α␈↓ π(␈↓ π⊂1.4.1 Formal Reasoning and Basic
␈↓ ↓H␈↓pattern of dialectical argumentation, in which␈↓ εh␈↓ πP␈↓α␈↓ πhArti␈↓␈↓βc␈↓␈↓αcial Intelligence
␈↓ ↓H␈↓one rule will construct a reason for acting on
␈↓ ↓H␈↓one option, a second rule will challenge that␈↓ εh␈↓John McCarthy will direct the work on formal
␈↓ ↓H␈↓reason, a third rule will challenge the ␈↓ εh␈↓reasoning and basic arti␈↓↓␈↓βC␈↓↓␈↓cial intelligence and
␈↓ ↓H␈↓challenging reason, and so on. For example,␈↓ εh␈↓will continue his own research in the
␈↓ ↓H␈↓ANALYST might counter the proposed ␈↓ εh␈↓epistemological problems of arti␈↓↓␈↓βC␈↓↓␈↓cial intelligence
␈↓ ↓H␈↓interpretation of Ivanov's return to Moscow␈↓ εh␈↓and the theory of program veri␈↓↓␈↓βC␈↓↓␈↓cation. Besides
␈↓ ↓H␈↓with an observation that the local police ␈↓ εh␈↓this he will take part in the speci␈↓↓␈↓βC␈↓↓␈↓cation and
␈↓ ↓H␈↓arrested a burglar who could implicate Ivanov␈↓ εh␈↓implementation of ANALYST.
␈↓ ↓H␈↓in several crimes. However, ANALYST might
␈↓ ↓H␈↓go further and counter this new interpretation␈↓ εh␈↓McCarthy's recent research e␈↓↓␈↓β@␈↓↓␈↓orts have mainly
␈↓ ↓H␈↓with the general fact that Ivanov is meticulous␈↓ εh␈↓involved extending the circumscription method
␈↓ ↓H␈↓about getting blackmail information about the␈↓ εh␈↓of non-monotonic reasoning described in
␈↓ ↓H␈↓local police chief wherever he goes. But this␈↓ εh␈↓[McCarthy 1980]. Formal methods of non-
␈↓ ↓H␈↓might in turn be countered by an observation␈↓ εh␈↓monotonic reasoning are a development of the
␈↓ ↓H␈↓that the previous police chief just retired, and␈↓ εh␈↓last ␈↓↓␈↓βC␈↓↓␈↓ve years.
␈↓ ↓H␈↓that there hasn't been enough time for Ivanov
␈↓ ↓H␈↓to investigate the new chief. These general␈↓ εh␈↓There is a good prospect for breakthroughs on
␈↓ ↓H␈↓rules are important in succinctly specifying␈↓ εh␈↓the long-standing ``quali␈↓↓␈↓βC␈↓↓␈↓cation problem'' in the
␈↓ ↓H␈↓special cases and exceptions to other general␈↓ εh␈↓next few years using circumscription and
␈↓ ↓H␈↓rules. This technique makes important use of␈↓ εh␈↓various generalizations. Two ideas are
␈↓ ↓H␈↓the maintenance and explanation facilities␈↓ εh␈↓involved.
␈↓ ↓H␈↓provided by reason maintenance techniques.
␈↓ ↓H␈↓We hope to combine these ideas with those of␈↓ εh␈↓First, frame axioms are derivable from a slight
␈↓ ↓H␈↓Gabriel on comparative matching of ␈↓ εh␈↓generalization of the circumscription method of
␈↓ ↓H␈↓descriptions to yield a powerful conjectural␈↓ εh␈↓[McCarthy 1980]. The generalized
␈↓ ↓H␈↓(heuristic) component that interacts cleanly with␈↓ εh␈↓circumscription gives a sentence schema stating
␈↓ ↓H␈↓a formal, deductive mechanism. ␈↓ εh␈↓that certain functions and predicates minimize
␈↓ εh␈↓the truth value of a certain sentence while
␈↓ ↓H␈↓α␈↓ βHPatterns ␈↓ εh␈↓holding other sentences true. It is a logical
␈↓ εh␈↓analog of the mathematical method of
␈↓ ↓H␈↓Many of the patterns ANALYST will have to ␈↓ εh␈↓minimization subject to constraints of the
␈↓ ↓H␈↓recognize do not fall into the categories so far␈↓ εh␈↓calculus of variations although it is not yet
␈↓ ↓H␈↓treated in AI work. For example, explaining␈↓ εh␈↓apparent that the analogy can be exploited. It
␈↓ ↓H␈↓an unknown activity of an adversary requires␈↓ εh␈↓allows us to specify that the only entities that
␈↓ ↓H␈↓conjecturing a goal and its relation to other␈↓ εh␈↓change when an event takes place are those
␈↓ ↓H␈↓goals, a belief structure that makes the goal␈↓ εh␈↓that the description of the event and associated
␈↓ ↓H␈↓seem desirable and attainable, and a means of␈↓ εh␈↓facts force to change. Circumscription permits
␈↓ ↓H␈↓attaining the goal that gives rise to the ␈↓ εh␈↓this to be done without an initial commitment
␈↓ ↓H␈↓observations. Present AI pattern recognition␈↓ εh␈↓as to what these facts will be.
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ J9
␈↓ ↓H␈↓For example, we can tell ANALYST that the ␈↓ εh␈↓to say that a sentence is unambiguous unless
␈↓ ↓H␈↓event of a person moving from one city to ␈↓ εh␈↓two interpretations are proposable. This will
␈↓ ↓H␈↓another leaves ␈↓↓␈↓βC␈↓↓␈↓xed everyone whom it doesn't␈↓ εh␈↓allow an intelligence specialist to tell
␈↓ ↓H␈↓say moves. The fact that a person's family␈↓ εh␈↓ANALYST about propensities to attempt to
␈↓ ↓H␈↓moves with him is then an add-on rather than␈↓ εh␈↓bribe without being aware that ambiguities are
␈↓ ↓H␈↓a modi␈↓↓␈↓βC␈↓↓␈↓cation. This meets the requirement␈↓ εh␈↓possible, and it will allow ANALYST to use
␈↓ ↓H␈↓that the person or computer program adding␈↓ εh␈↓the concept without problem until and unless
␈↓ ↓H␈↓the fact that when a person moves his family␈↓ εh␈↓ambiguous examples actually arise.
␈↓ ↓H␈↓also moves need not understand the initial
␈↓ ↓H␈↓axiom giving the e␈↓↓␈↓β@␈↓↓␈↓ects of moving. It is a key␈↓ εh␈↓McCarthy will also continue his research on the
␈↓ ↓H␈↓property of intelligent systems that they can be␈↓ εh␈↓ELEPHANT formalism for representing
␈↓ ↓H␈↓advised and their behavior modi␈↓↓␈↓βC␈↓↓␈↓ed by ␈↓ εh␈↓sequential programs in ␈↓↓␈↓βC␈↓↓␈↓rst order logic.
␈↓ ↓H␈↓someone who does not understand the details of
␈↓ ↓H␈↓how they work. It will be especially important␈↓ εh␈↓Goals and milestones
␈↓ ↓H␈↓when knowledge representation and problem
␈↓ ↓H␈↓solving systems like ANALYST contain many ␈↓ εh␈↓⊗ December 1981 Completion of paper on
␈↓ ↓H␈↓tens of thousands of facts. ␈↓ εh␈↓ELEPHANT.
␈↓ ↓H␈↓The second new application of circumscription␈↓ εh␈↓⊗ June 1982 Completion of paper on use of
␈↓ ↓H␈↓is more di␈↓↓␈↓β@␈↓↓␈↓icult but probably more far- ␈↓ εh␈↓circumscription to get ``ambiguity tolerance''.
␈↓ ↓H␈↓reaching. Suppose we need to tell ANALYST
␈↓ ↓H␈↓that the Russians sometimes attempt to bribe␈↓ εh␈↓α␈↓ π(␈↓ π"1.4.2 Representations and Reasoning:
␈↓ ↓H␈↓foreign o␈↓↓␈↓β@␈↓↓␈↓icials to reveal secrets and that they␈↓ εh␈↓ π=␈↓α␈↓ πhTheoretical Foundations
␈↓ ↓H␈↓can be embarassed when such attempts are
␈↓ ↓H␈↓revealed. This seems straightforward and a␈↓ εh␈↓Lewis Creary is continuing his work on the
␈↓ ↓H␈↓human would have no di␈↓↓␈↓β@␈↓↓␈↓iculty absorbing the␈↓ εh␈↓epistemology of arti␈↓↓␈↓βC␈↓↓␈↓cial intelligence and the
␈↓ ↓H␈↓information. However, for any present ␈↓ εh␈↓representation of knowledge, with the current
␈↓ ↓H␈↓knowledge representation system to accept the␈↓ εh␈↓overall goal being twofold:
␈↓ ↓H␈↓information, a number of very pedantic issues
␈↓ ↓H␈↓would have to be resolved: (1) ␈↓↓Does attempting␈↓ εh␈↓1. to formalize the main concepts involved in
␈↓ ↓H␈↓↓to bribe an o␈↓␈↓βP␈↓␈↓↓icial include o␈↓␈↓βP␈↓␈↓↓ering a bribe to␈↓ εh␈↓␈↓ π_the planning of actions, and to provide a
␈↓ ↓H␈↓↓someone who is mistakenly believed to be an␈↓ εh␈↓␈↓ π_sound truth-theoretic semantics for the
␈↓ ↓H␈↓↓o␈↓␈↓βP␈↓␈↓↓icial? (2) Does it include o␈↓␈↓βP␈↓␈↓↓ering a bribe to␈↓ εh␈↓␈↓ π_resulting representations [Creary 1981d].
␈↓ ↓H␈↓↓someone who is not believed to be an o␈↓␈↓βP␈↓␈↓↓icial but␈↓ εh␈↓␈↓ π_This will include treatments of:
␈↓ ↓H␈↓↓turns out to be? Must there be an individual
␈↓ ↓H␈↓↓who is o␈↓␈↓βP␈↓␈↓↓ered the bribe or can letting it be known␈↓ εh␈↓␈↓ π_a. actions, events, situations, properties, and
␈↓ ↓H␈↓↓that a bribe is available count as an attempt to␈↓ εh␈↓␈↓ πHtemporal relationships
␈↓ ↓H␈↓↓bribe an o␈↓␈↓βP␈↓␈↓↓icial␈↓? Intuitively, all these issues
␈↓ ↓H␈↓seem to be irrelevant. They probably won't␈↓ εh␈↓␈↓ π_b. counterfactual planning conditionals
␈↓ ↓H␈↓come up, and if they did, they could be
␈↓ ↓H␈↓resolved in an ad hoc way. However, present␈↓ εh␈↓␈↓ π_c. causal relations among actions, events,
␈↓ ↓H␈↓knowledge representation systems require ␈↓ εh␈↓␈↓ πHand causal in␈↓↓␈↓βD␈↓↓␈↓uences (i.e., generalized
␈↓ ↓H␈↓de␈↓↓␈↓βC␈↓↓␈↓nitions applicable to all cases. ␈↓ εh␈↓␈↓ πHforces).
␈↓ ↓H␈↓Circumscription and other forms of non- ␈↓ εh␈↓␈↓ π_d. propositional attitudes (largely complete;
␈↓ ↓H␈↓monotonic reasoning apparently allow us to␈↓ εh␈↓␈↓ πHsee [Creary 1979])
␈↓ ↓H␈↓make systems that may be characterized as
␈↓ ↓H␈↓``ambiguity tolerant'' - something that Hubert␈↓ εh␈↓2. to provide a sound epistemological basis for
␈↓ ↓H␈↓Dreyfus said was impossible for computers.␈↓ εh␈↓␈↓ π_commonsense reasoning involving the
␈↓ ↓H␈↓The idea, not yet well worked out, is to be able␈↓ εh␈↓␈↓ π_above notions in general, and causal
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ >10
␈↓ ↓H␈↓␈↓ ↓xreasoning in particular. [Creary 1981b] is a␈↓ εh␈↓commonsense factual reasoning, suggests that
␈↓ ↓H␈↓␈↓ ↓x␈↓↓␈↓βC␈↓↓␈↓rst step in this direction (the ideas ␈↓ εh␈↓problem solvers using the new ideas may be
␈↓ ↓H␈↓␈↓ ↓xinvolved are brie␈↓↓␈↓βD␈↓↓␈↓y discussed in point 4 of␈↓ εh␈↓able to treat naturally some problems of the sort
␈↓ ↓H␈↓␈↓ ↓xthe following subsection). Applications and␈↓ εh␈↓that ANALYST (see section 1.3) might face ␈↓↓␈↓βE␈↓↓␈↓
␈↓ ↓H␈↓␈↓ ↓xextensions of the framework presented in ␈↓ εh␈↓problems that are inaccessible to or awkward
␈↓ ↓H␈↓␈↓ ↓xthat paper will include: ␈↓ εh␈↓for previous general problem solvers. These
␈↓ εh␈↓problems include those whose solution requires
␈↓ ↓H␈↓␈↓ ↓xa. extension of the general theory of ␈↓ εh␈↓non-trivial reasoning concerning the beliefs
␈↓ ↓H␈↓␈↓ α(``competing considerations'' to cover ␈↓ εh␈↓and desires of other organisms, and those
␈↓ ↓H␈↓␈↓ α(various kinds of non-factual reasoning ␈↓ εh␈↓requiring the making of reasonable, but fallible,
␈↓ εh␈↓conjectures. Checking this requires experiment.
␈↓ ↓H␈↓␈↓ ↓xb. specialization of the general theory to
␈↓ ↓H␈↓␈↓ α(deal with causal reasoning, the ␈↓ εh␈↓Creary's earlier design studies toward an
␈↓ ↓H␈↓␈↓ α(counterfactually conditional conclusions ␈↓ εh␈↓advice-taking problem solver that implements
␈↓ ↓H␈↓␈↓ α(involved in AI planning applications, ␈↓ εh␈↓these theoretical developments have recently
␈↓ ↓H␈↓␈↓ α(and the frame and quali␈↓↓␈↓βC␈↓↓␈↓cation ␈↓ εh␈↓been found to be compatible with and
␈↓ ↓H␈↓␈↓ α(problems [Creary 1981c]. ␈↓ εh␈↓complementary to some ideas and associated
␈↓ εh␈↓software developed by Richard Gabriel as part
␈↓ ↓H␈↓␈↓ ↓xc. applications involving detailed ␈↓ εh␈↓of his doctoral research on the organization of
␈↓ ↓H␈↓␈↓ α(investigation of particular problems, for ␈↓ εh␈↓very large intelligent programs. Since Gabriel
␈↓ ↓H␈↓␈↓ α(which speci␈↓↓␈↓βC␈↓↓␈↓c sets of epistemic statuses ␈↓ εh␈↓has recently joined the formal reasoning group
␈↓ ↓H␈↓␈↓ α(and consideration types will be ␈↓ εh␈↓as a collaborator on this project, it now appears
␈↓ ↓H␈↓␈↓ α(developed. The reasoning involved will ␈↓ εh␈↓that the most e␈↓↓␈↓β@␈↓↓␈↓icient route to an initial
␈↓ ↓H␈↓␈↓ α(deal with the planning of ␈↓ εh␈↓implementation is to rework, for our purposes,
␈↓ ↓H␈↓␈↓ α(communications and travel problems, ␈↓ εh␈↓some of his existing domain-independent
␈↓ ↓H␈↓␈↓ α(and will involve both causal reasoning, ␈↓ εh␈↓problem-solving software.
␈↓ ↓H␈↓␈↓ α(and the sort of simulative reasoning
␈↓ ↓H␈↓␈↓ α(about the propositional attitudes of ␈↓ εh␈↓α␈↓ ↓Goal
␈↓ ↓H␈↓␈↓ α(others that is discussed in point 6 of the
␈↓ ↓H␈↓␈↓ α(following subsection. These ␈↓ εh␈↓⊗ We propose to construct an advanced,
␈↓ ↓H␈↓␈↓ α(investigations will be conducted in ␈↓ εh␈↓advice-taking problem solver for analyzing
␈↓ ↓H␈↓␈↓ α(conjunction with work on the advice- ␈↓ εh␈↓interesting kinds of ``intelligence'' information ␈↓↓␈↓βE␈↓↓␈↓
␈↓ ↓H␈↓␈↓ α(taking ANALYST program (see next ␈↓ εh␈↓in short, a ␈↓↓␈↓βC␈↓↓␈↓rst incarnation of ANALYST.
␈↓ ↓H␈↓␈↓ α(subsection), which will supply the ␈↓ εh␈↓This program will attempt to infer concealed
␈↓ ↓H␈↓␈↓ α(detailed stimulation and feedback ␈↓ εh␈↓facts from visible facts and reasonable
␈↓ ↓H␈↓␈↓ α(needed. ␈↓ εh␈↓conjectures that it has made. It will deal with
␈↓ εh␈↓information about beliefs, desires, purposes,
␈↓ ↓H␈↓Almost all of the theoretical developments just␈↓ εh␈↓preferences, aversions, and fears. It will both
␈↓ ↓H␈↓discussed will be be directly applied in the new␈↓ εh␈↓ascribe purposes to actions and use ascribed
␈↓ ↓H␈↓advice-taking ANALYST program (see next ␈↓ εh␈↓purposes to predict actions. It will sometimes
␈↓ ↓H␈↓subsection), on which Creary is also working.␈↓ εh␈↓infer the existence of previously unknown
␈↓ εh␈↓hidden entities from their observed e␈↓↓␈↓β@␈↓↓␈↓ects.
␈↓ ↓H␈↓α␈↓ αλ␈↓ α∂1.4.3 An Advice-Taking ANALYST
␈↓ ↓H␈↓ β¬␈↓α␈↓ αHProgram ␈↓ εh␈↓An important skill of a human ANALYST,
␈↓ εh␈↓which we hope to model, is the ability to infer
␈↓ ↓H␈↓Recent progress by McCarthy and Lewis ␈↓ εh␈↓the goals and plans of other people from the
␈↓ ↓H␈↓Creary in formalizing knowledge about ␈↓ εh␈↓facts of their actions. At this point there are
␈↓ ↓H␈↓propositional attitudes, by McCarthy in ␈↓ εh␈↓several distinctions that need to be made with
␈↓ ↓H␈↓formalizing the new method of circumscription,␈↓ εh␈↓respect to the inference or recognition problem.
␈↓ ↓H␈↓and by Creary in explicating the structure of␈↓ εh␈↓A ␈↓↓plan␈↓ is more than simply an orderly
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ @11
␈↓ ↓H␈↓arrangement of actions; it is an orderly ␈↓ εh␈↓Still more speci␈↓↓␈↓βC␈↓↓␈↓cally, we wish to investigate the
␈↓ ↓H␈↓arrangement plus an association of the actions␈↓ εh␈↓problem-solving power of the new ideas
␈↓ ↓H␈↓to goals and subgoals of the actor (the person␈↓ εh␈↓mentioned above concerning
␈↓ ↓H␈↓making the plan). To infer a plan as an orderly␈↓ εh␈↓a) the representation of facts about knowledge,
␈↓ ↓H␈↓arrangement of known actions is simple: it is␈↓ εh␈↓␈↓ π_belief, and desire,
␈↓ ↓H␈↓simply the orderly arrangement of those actions.␈↓ εh␈↓b) the form of various kinds of conjectural
␈↓ ↓H␈↓The interesting cases are where the goals are␈↓ εh␈↓␈↓ π_reasoning,
␈↓ ↓H␈↓not all known and/or not all of the actions are
␈↓ ↓H␈↓known. In the case that the goals are known␈↓ εh␈↓A related, but somewhat di␈↓↓␈↓β@␈↓↓␈↓erent, motivation is
␈↓ ↓H␈↓but not all of the actions known is called ␈↓↓plan␈↓ εh␈↓the desire to determine where the weakest
␈↓ ↓H␈↓↓recognition␈↓. In the case that not all of the goals␈↓ εh␈↓threads are in the fabric of current AI heuristic
␈↓ ↓H␈↓are known is called ␈↓↓goal-plan recognition␈↓.␈↓ εh␈↓technology ␈↓↓␈↓βE␈↓↓␈↓ especially in relation to the
␈↓ εh␈↓solution of problems of the type
␈↓ ↓H␈↓Goal-plan recognition is quite formidable since␈↓ εh␈↓characteristically investigated by our group.
␈↓ ↓H␈↓it is a superset of the plan production problem.
␈↓ ↓H␈↓Furthermore, in the ANALYST problem there ␈↓ εh␈↓α␈↓ λ8Design Criteria
␈↓ ↓H␈↓is the need to deduce the motivations for the
␈↓ ↓H␈↓goals and plan, to locate unusual aspects of the␈↓ εh␈↓A. The problem solver should provide a
␈↓ ↓H␈↓actions involved in the plan, and to deduce the␈↓ εh␈↓␈↓ π_convenient and e␈↓↓␈↓β@␈↓↓␈↓ective test bed and
␈↓ ↓H␈↓underlying, deliberately hidden motivations for␈↓ εh␈↓␈↓ π_development tool for the research conducted
␈↓ ↓H␈↓those aspects. Thus, the ANALYST subsumes␈↓ εh␈↓␈↓ π_by members of the AI & Formal Reasoning
␈↓ ↓H␈↓the abilities of a planning/problem solving␈↓ εh␈↓␈↓ π_Group. Accordingly, it should emphasize
␈↓ ↓H␈↓agent with signi␈↓↓␈↓βC␈↓↓␈↓cant further abilities. ␈↓ εh␈↓␈↓ π_(but not overemphasize) the role of logic in
␈↓ εh␈↓␈↓ π_problem solving, and should facilitate the
␈↓ ↓H␈↓Since it is unreasonable to expect that the set of␈↓ εh␈↓␈↓ π_evaluation and improvement of ideas and
␈↓ ↓H␈↓general facts about peoples' activities along with␈↓ εh␈↓␈↓ π_techniques developed within the group.
␈↓ ↓H␈↓the speci␈↓↓␈↓βC␈↓↓␈↓c habits and traits of particular
␈↓ ↓H␈↓people of interest to ANALYST can or should␈↓ εh␈↓B. The design should re␈↓↓␈↓βD␈↓↓␈↓ect the present state
␈↓ ↓H␈↓be procedurally encoded within reasoning ␈↓ εh␈↓␈↓ π_of the art in problem solving. We don't
␈↓ ↓H␈↓programs, and since the addition of new ␈↓ εh␈↓␈↓ π_want to re-invent anything, or (still worse)
␈↓ ↓H␈↓information, both by ANALYST itself and by␈↓ εh␈↓␈↓ π_to have readily avoidable de␈↓↓␈↓βC␈↓↓␈↓ciencies in the
␈↓ ↓H␈↓the human interacting with the program, ␈↓ εh␈↓␈↓ π_program. We want to provide the best
␈↓ ↓H␈↓should be quick and easy, an Advice-Taker ␈↓ εh␈↓␈↓ π_possible problem-solving environment in
␈↓ ↓H␈↓style program, with facts represented in a␈↓ εh␈↓␈↓ π_which to try out our ideas.
␈↓ ↓H␈↓modular, formal representation is strongly
␈↓ ↓H␈↓indicated. ␈↓ εh␈↓C. The problem solver should be readily
␈↓ εh␈↓␈↓ π_revisable, in order to facilitate and
␈↓ ↓H␈↓α␈↓ β6Motivation ␈↓ εh␈↓␈↓ π_encourage experimentation with a number
␈↓ εh␈↓␈↓ π_of di␈↓↓␈↓β@␈↓↓␈↓erent problem-solving designs. This
␈↓ ↓H␈↓In general, we wish to keep our thinking in␈↓ εh␈↓␈↓ π_ease of revision is essential if the problem
␈↓ ↓H␈↓touch with the prime criterion of value for␈↓ εh␈↓␈↓ π_solver is to function over a signi␈↓↓␈↓βC␈↓↓␈↓cant
␈↓ ↓H␈↓ideas in arti␈↓↓␈↓βC␈↓↓␈↓cial intelligence: their contribution␈↓ εh␈↓␈↓ π_period of time as a truly useful research
␈↓ ↓H␈↓to the successful performance of problem- ␈↓ εh␈↓␈↓ π_tool. The way to achieve this goal is to
␈↓ ↓H␈↓solving, question-answering, and learning ␈↓ εh␈↓␈↓ π_design the program in such a way that
␈↓ ↓H␈↓programs. ␈↓ εh␈↓␈↓ π_those conceptually independent features of
␈↓ εh␈↓␈↓ π_it which might be subject to change
␈↓ ↓H␈↓More speci␈↓↓␈↓βC␈↓↓␈↓cally, we wish to be able to test␈↓ εh␈↓␈↓ π_(memory retrieval algorithm, problem
␈↓ ↓H␈↓realistically (and, when possible, to demonstrate)␈↓ εh␈↓␈↓ π_solving control structure, etc.,) are variable
␈↓ ↓H␈↓the problem-solving power of ideas, ␈↓ εh␈↓␈↓ π_independently of one another in the
␈↓ ↓H␈↓approaches, and techniques developed within␈↓ εh␈↓␈↓ π_program, and are represented by easily
␈↓ ↓H␈↓the AI & Formal Reasoning Group.
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ >12
␈↓ ↓H␈↓␈↓ ↓xvariable program elements such as ␈↓ εh␈↓``Advice Taker'' program essentially along the
␈↓ ↓H␈↓␈↓ ↓xproduction rules, parameter tables, etc. The␈↓ εh␈↓lines ␈↓↓␈↓βC␈↓↓␈↓rst laid down in his paper ``Programs
␈↓ ↓H␈↓␈↓ ↓ximplication of this approach is that we ␈↓ εh␈↓with Common Sense'' [1959], and extended in
␈↓ ↓H␈↓␈↓ ↓xshould try to design, not a particular ␈↓ εh␈↓[McCarthy and Hayes 1969] and subsequent
␈↓ ↓H␈↓␈↓ ↓xproblem solver, but a system or framework ␈↓ εh␈↓papers by McCarthy. A review of the Advice-
␈↓ ↓H␈↓␈↓ ↓xfor problem solving that can be ␈↓ εh␈↓Taker design in the light of currently available
␈↓ ↓H␈↓␈↓ ↓x``programmed'' to instantiate any of a large␈↓ εh␈↓AI techniques suggests that many of its basic
␈↓ ↓H␈↓␈↓ ↓xnumber of particular problem solvers. ␈↓ εh␈↓concepts are sound and viable, and that
␈↓ ↓H␈↓␈↓ ↓xConcern with this issue need not bog us ␈↓ εh␈↓prospects for a successful implementation are
␈↓ ↓H␈↓␈↓ ↓xdown in system building, however; it should␈↓ εh␈↓good. More speci␈↓↓␈↓βC␈↓↓␈↓cally, we intend to
␈↓ ↓H␈↓␈↓ ↓xbe possible to start by writing a particular␈↓ εh␈↓incorporate the following high-level design
␈↓ ↓H␈↓␈↓ ↓xproblem solver with built-in generalization␈↓ εh␈↓ideas into our initial implementation:
␈↓ ↓H␈↓␈↓ ↓xpoints. The important thing is to keep this
␈↓ ↓H␈↓␈↓ ↓xdesign goal in mind from the beginning. ␈↓ εh␈↓1. ␈↓↓A general framework for the structuring,
␈↓ εh␈↓↓␈↓ π_description, and use of specialized knowledge
␈↓ ↓H␈↓α␈↓ αPRelation to FOL and EKL ␈↓ εh␈↓↓␈↓ π_as the foundation for a meta-general problem
␈↓ εh␈↓↓␈↓ π_solver␈↓. Much knowledge properly
␈↓ ↓H␈↓The elementary parts of FOL and EKL, on one␈↓ εh␈↓␈↓ π_distributed throughout memory in ␈↓↓concepts␈↓
␈↓ ↓H␈↓hand, and the proposed new problem solver, on␈↓ εh␈↓␈↓ π_is required for a system to reason e␈↓↓␈↓β@␈↓↓␈↓ectively
␈↓ ↓H␈↓the other, are the tools of di␈↓↓␈↓β@␈↓↓␈↓erent, ␈↓ εh␈↓␈↓ π_and e␈↓↓␈↓β@␈↓↓␈↓iciently about the means of achieving
␈↓ ↓H␈↓complementary approaches to research in ␈↓ εh␈↓␈↓ π_desired goals, and to analyze intelligently
␈↓ ↓H␈↓arti␈↓↓␈↓βC␈↓↓␈↓cial intelligence. In their simplest form,␈↓ εh␈↓␈↓ π_information concerning the behavior of
␈↓ ↓H␈↓FOL and EKL may be viewed as the proof- ␈↓ εh␈↓␈↓ π_potential adversaries.
␈↓ ↓H␈↓checking component in McCarthy and Hayes's
␈↓ ↓H␈↓[1969] ``Missouri program'' (MP), and as such is␈↓ εh␈↓2. ␈↓↓Interactive advice seeking and taking as a
␈↓ ↓H␈↓a tool of epistemological research; such research␈↓ εh␈↓↓␈↓ π_means of knowledge acquisition␈↓. According
␈↓ ↓H␈↓may (and probably should) be carried quite␈↓ εh␈↓␈↓ π_to McCarthy's 1959 conception of it, advice
␈↓ ↓H␈↓some distance in abstraction from heuristic␈↓ εh␈↓␈↓ π_taking is a form of goal-directed
␈↓ ↓H␈↓issues before attempts are made to implement␈↓ εh␈↓␈↓ π_information transfer. The goal is to
␈↓ ↓H␈↓ideas in a full problem-solving context. On the␈↓ εh␈↓␈↓ π_improve the performance of the advice
␈↓ ↓H␈↓other hand, the proposed new problem solver is␈↓ εh␈↓␈↓ π_taker by giving it information (advice), in a
␈↓ ↓H␈↓a version of McCarthy and Hayes's ``reasoning␈↓ εh␈↓␈↓ π_manner that requires of the advice giver
␈↓ ↓H␈↓program'' (RP), and, in the presence of basic␈↓ εh␈↓␈↓ π_``little if any knowledge of the program or
␈↓ ↓H␈↓proof-checkers, can be reserved for study of the␈↓ εh␈↓␈↓ π_the previous knowledge of the advice
␈↓ ↓H␈↓primarily heuristic aspects of a given class of␈↓ εh␈↓␈↓ π_taker''. Under these conditions, it is
␈↓ ↓H␈↓problems. It is to be expected that research␈↓ εh␈↓␈↓ π_unlikely that the advice giver will be very
␈↓ ↓H␈↓economies will be achieved by using the two␈↓ εh␈↓␈↓ π_good at guessing what knowledge the
␈↓ ↓H␈↓components thus in tandem, since it will ␈↓ εh␈↓␈↓ π_program needs in order to improve its
␈↓ ↓H␈↓probably be cheaper to check the ␈↓ εh␈↓␈↓ π_performance in the desired way. This
␈↓ ↓H␈↓epistemological adequacy of ideas with FOL or␈↓ εh␈↓␈↓ π_suggests that an interactive exchange is
␈↓ ↓H␈↓EKL than with the problem solver. Moreover,␈↓ εh␈↓␈↓ π_needed between the advice giver and taker,
␈↓ ↓H␈↓this division of labor will permit individual␈↓ εh␈↓␈↓ π_in which the giver ␈↓↓␈↓βC␈↓↓␈↓rst sets the
␈↓ ↓H␈↓researchers to focus closely on manageable␈↓ εh␈↓␈↓ π_improvement goals, and the program then
␈↓ ↓H␈↓subparts of a given AI problem. ␈↓ εh␈↓␈↓ π_determines what new knowledge, if any, it
␈↓ εh␈↓␈↓ π_needs to be able to make the speci␈↓↓␈↓βC␈↓↓␈↓ed
␈↓ ↓H␈↓α␈↓ α⊗Basic Approach and Leading Ideas ␈↓ εh␈↓␈↓ π_improvements with a reasonable amount of
␈↓ εh␈↓␈↓ π_e␈↓↓␈↓β@␈↓↓␈↓ort, and asks for it. The ability to seek
␈↓ ↓H␈↓Our basic approach to construction of an ␈↓ εh␈↓␈↓ π_advice is to be based on the program's
␈↓ ↓H␈↓ANALYST will be to use state-of-the-art AI␈↓ εh␈↓␈↓ π_meta-knowledge of its own knowledge and
␈↓ ↓H␈↓techniques to implement John McCarthy's ␈↓ εh␈↓␈↓ π_capabilities. The ability to take advice is to
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ >13
␈↓ ↓H␈↓␈↓ ↓xbe based on the program's ability to ␈↓ εh␈↓␈↓ π_conclusion is justi␈↓↓␈↓βC␈↓↓␈↓ed only if a reasonable
␈↓ ↓H␈↓␈↓ ↓x``compile'' received advice into the most ␈↓ εh␈↓␈↓ π_e␈↓↓␈↓β@␈↓↓␈↓ort has been made to discover all states
␈↓ ↓H␈↓␈↓ ↓xappropriate form for its own internal use.␈↓ εh␈↓␈↓ π_of a␈↓↓␈↓β@␈↓↓␈↓airs that are causally relevant to it (``Is
␈↓ ↓H␈↓␈↓ ↓xOne important mechanism by which advice ␈↓ εh␈↓␈↓ π_anything wrong with the boat that would
␈↓ ↓H␈↓␈↓ ↓xcan be brought to bear on problem solving ␈↓ εh␈↓␈↓ π_tend to prevent its use in the normal way?'').
␈↓ ↓H␈↓␈↓ ↓xis through the descriptions involved in ␈↓ εh␈↓␈↓ π_This approach to the frame and
␈↓ ↓H␈↓␈↓ ↓xcomparative partial matching (see 5 below).␈↓ εh␈↓␈↓ π_quali␈↓↓␈↓βC␈↓↓␈↓cation problems eliminates frame
␈↓ εh␈↓␈↓ π_axioms and overly long quali␈↓↓␈↓βC␈↓↓␈↓cations of
␈↓ ↓H␈↓3. ␈↓↓Integration of the frames/units and predicate␈↓ εh␈↓␈↓ π_preconditions in favor of implicit meta-
␈↓ ↓H␈↓↓␈↓ ↓xcalculus approaches to knowledge ␈↓ εh␈↓␈↓ π_premises that all reasonably discoverable
␈↓ ↓H␈↓↓␈↓ ↓xrepresentation␈↓. Though frame- and unit- ␈↓ εh␈↓␈↓ π_relevant considerations have been taken
␈↓ ↓H␈↓␈↓ ↓xbased styles of representation are often ␈↓ εh␈↓␈↓ π_into account.
␈↓ ↓H␈↓␈↓ ↓xcontrasted with predicate calculus
␈↓ ↓H␈↓␈↓ ↓xrepresentations, there is no inherent ␈↓ εh␈↓5. ␈↓↓Comparative partial matching as the basis for
␈↓ ↓H␈↓␈↓ ↓xincompatibility between the two, as has ␈↓ εh␈↓↓␈↓ π_selection of the most appropriate methods,
␈↓ ↓H␈↓␈↓ ↓xsometimes been noticed in the AI literature.␈↓ εh␈↓↓␈↓ π_procedures, abstract plan schemata, etc.,
␈↓ ↓H␈↓␈↓ ↓xWhat has not been attempted, however, and ␈↓ εh␈↓↓␈↓ π_during problem solving␈↓. Judgments of
␈↓ ↓H␈↓␈↓ ↓xwhat we intend to achieve for the ␈↓ εh␈↓␈↓ π_appropriateness involve bringing multiple
␈↓ ↓H␈↓␈↓ ↓xANALYST, is a thoroughgoing logical ␈↓ εh␈↓␈↓ π_goals and constraints to bear in a way that
␈↓ ↓H␈↓␈↓ ↓xinterpretation of every signi␈↓↓␈↓βC␈↓↓␈↓cant aspect of␈↓ εh␈↓␈↓ π_permits each single goal or constraint to
␈↓ ↓H␈↓␈↓ ↓xa unit-style representation. The basic ␈↓ εh␈↓␈↓ π_␈↓↓in␈↓␈↓βT␈↓␈↓↓uence␈↓ the judgment without completely
␈↓ ↓H␈↓␈↓ ↓xorganizing structure of ANALYST's ␈↓ εh␈↓␈↓ π_determining it. Partial and comparative
␈↓ ↓H␈↓␈↓ ↓xmemory will be the ␈↓↓concept␈↓, which is ␈↓ εh␈↓␈↓ π_matching, where that matching is
␈↓ ↓H␈↓␈↓ ↓xessentially an indexed set of propositions␈↓ εh␈↓␈↓ π_intelligently managed, can be used as a
␈↓ ↓H␈↓␈↓ ↓xand procedures (or propositional and ␈↓ εh␈↓␈↓ π_vehicle for making such judgments (cf.
␈↓ ↓H␈↓␈↓ ↓xprocedural schemata), which itself serves as␈↓ εh␈↓␈↓ π_[Gabriel 1980] and [Hayes-Roth 1978]).
␈↓ ↓H␈↓␈↓ ↓xa higher-level indexing entry for its ␈↓ εh␈↓␈↓ π_The essential idea is that by fully and
␈↓ ↓H␈↓␈↓ ↓xcontents. In general, concepts have a logical␈↓ εh␈↓␈↓ π_properly describing a situation, one is able
␈↓ ↓H␈↓␈↓ ↓xform and an associated truth-theoretic ␈↓ εh␈↓␈↓ π_to locate and incorporate techniques and
␈↓ ↓H␈↓␈↓ ↓xsemantics, and are to be implemented as ␈↓ εh␈↓␈↓ π_facts that bear upon several aspects of that
␈↓ ↓H␈↓␈↓ ↓x␈↓↓units␈↓. Part of the indexing associated with␈↓ εh␈↓␈↓ π_situation at the same time; similarly,
␈↓ ↓H␈↓␈↓ ↓xa concept is a set of descriptions and/or ␈↓ εh␈↓␈↓ π_multiple motivations can be weighed and
␈↓ ↓H␈↓␈↓ ↓xabstractions of its content, which are to ␈↓ εh␈↓␈↓ π_explicit tradeo␈↓↓␈↓β@␈↓↓␈↓s considered.
␈↓ ↓H␈↓␈↓ ↓xserve as ``advertisements'' of the concept for
␈↓ ↓H␈↓␈↓ ↓xuse in partial comparative matching. ␈↓ εh␈↓6. ␈↓↓Fregean representation of propositional
␈↓ εh␈↓↓␈↓ π_attitudes, coupled with the simulative use of
␈↓ ↓H␈↓4. ␈↓↓A ``competing considerations'' analysis of␈↓ εh␈↓↓␈↓ π_the program's own human-like thought
␈↓ ↓H␈↓↓␈↓ ↓xcausal reasoning as the basis for solution of␈↓ εh␈↓↓␈↓ π_mechanisms as a means of recognizing and
␈↓ ↓H␈↓↓␈↓ ↓xthe frame and quali␈↓␈↓βS␈↓␈↓↓cation problems␈↓. Causal␈↓ εh␈↓↓␈↓ π_analyzing the beliefs, desires, plans, and
␈↓ ↓H␈↓␈↓ ↓xreasoning is a special form of ␈↓↓commonsense␈↓ εh␈↓↓␈↓ π_intentions of people and other intelligent
␈↓ ↓H␈↓↓␈↓ ↓xfactual reasoning␈↓, in which the drawing of␈↓ εh␈↓↓␈↓ π_organisms␈↓. Information concerning
␈↓ ↓H␈↓␈↓ ↓xconclusions results from the weighing and ␈↓ εh␈↓␈↓ π_propositional attitudes is to be represented
␈↓ ↓H␈↓␈↓ ↓xcomposition of all reasonably discoverable␈↓ εh␈↓␈↓ π_declaratively, in an extended version of
␈↓ ↓H␈↓␈↓ ↓xrelevant considerations (cf. [Creary 1981b]).␈↓ εh␈↓␈↓ π_McCarthy's ␈↓↓␈↓βC␈↓↓␈↓rst-order theory of individual
␈↓ ↓H␈↓␈↓ ↓xCausal sub-considerations arise from the ␈↓ εh␈↓␈↓ π_concepts and propositions (see [McCarthy
␈↓ ↓H␈↓␈↓ ↓xdiscovery of general states of a␈↓↓␈↓β@␈↓↓␈↓airs (i.e.,␈↓ εh␈↓␈↓ π_1979] and [Creary 1979]). This notation
␈↓ ↓H␈↓␈↓ ↓xpatterns of facts) that are known to give rise␈↓ εh␈↓␈↓ π_provides a powerful, systematic, and
␈↓ ↓H␈↓␈↓ ↓xin a lawlike way to causal in␈↓↓␈↓βD␈↓↓␈↓uences ␈↓ εh␈↓␈↓ π_intuitively motivated way of dealing with
␈↓ ↓H␈↓␈↓ ↓x(generalized forces) bearing on the truth of␈↓ εh␈↓␈↓ π_apparent failures of extensionality and
␈↓ ↓H␈↓␈↓ ↓xa given target proposition. A causal ␈↓ εh␈↓␈↓ π_quanti␈↓↓␈↓βC␈↓↓␈↓cation into intentional constructions.
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ ;14
␈↓ ↓H␈↓␈↓ ↓xThe sort of information that the framework␈↓ εh␈↓The above ability will accomplish the goal of
␈↓ ↓H␈↓␈↓ ↓xis meant to handle is illustrated by the ␈↓ εh␈↓establishing an ␈↓↓advice taker␈↓ methodology, along
␈↓ ↓H␈↓␈↓ ↓xcontent of this sentence: ␈↓↓ ``Ivanov believes␈↓ εh␈↓with representations and procedures for
␈↓ ↓H␈↓↓␈↓ ↓xthat none of the authors of the coded message␈↓ εh␈↓comparative matching, etc. The next step will
␈↓ ↓H␈↓↓␈↓ ↓xknows that the code has been broken.''␈↓ The␈↓ εh␈↓be to expand the capabilities of the problem-
␈↓ ↓H␈↓␈↓ ↓xfeatures of this sentence that are of special␈↓ εh␈↓solver to include ␈↓↓simple plan recognition␈↓: the
␈↓ ↓H␈↓␈↓ ↓xinterest here are i) the nesting or iteration␈↓ εh␈↓attribution of a plan to an agent given his
␈↓ ↓H␈↓␈↓ ↓xof propositional attitudes (``knows'' within␈↓ εh␈↓partial behavior and his known goals. Thus,
␈↓ ↓H␈↓␈↓ ↓xthe scope of ``believes''), ii) the occurrence of␈↓ εh␈↓from a set of actions and known goals, we want
␈↓ ↓H␈↓␈↓ ↓xa quanti␈↓↓␈↓βC␈↓↓␈↓er (``none'') within the scope of a␈↓ εh␈↓our system to supply the remaining actions in
␈↓ ↓H␈↓␈↓ ↓xverb of propositional attitude (``believes''),␈↓ εh␈↓the plan.
␈↓ ↓H␈↓␈↓ ↓xand iii) the occurrence of de␈↓↓␈↓βC␈↓↓␈↓nite
␈↓ ↓H␈↓␈↓ ↓xdescriptions (e.g., ``the coded message'')␈↓ εh␈↓Next we want to include goal discovery as a
␈↓ ↓H␈↓␈↓ ↓xwithin the scope of ``believes''. ␈↓ εh␈↓further aspect of the recognition task. Further
␈↓ ↓H␈↓␈↓ ↓xInstead of redundantly re-representing ␈↓ εh␈↓capabilities include discovering unusual or
␈↓ ↓H␈↓␈↓ ↓ximplicative connections among propositions␈↓ εh␈↓contrary to habit aspects of the plan
␈↓ ↓H␈↓␈↓ ↓xby means of declarative axioms at higher ␈↓ εh␈↓implementation, which will be used to reveal
␈↓ ↓H␈↓␈↓ ↓xlevels in the hierarchy of concepts, such ␈↓ εh␈↓hidden goals of the external agent. We call
␈↓ ↓H␈↓␈↓ ↓xinformation is simply to be utilized as ␈↓ εh␈↓these three capabilities: ␈↓↓simple plan recognition,
␈↓ ↓H␈↓␈↓ ↓xembedded in the program's own ordinary ␈↓ εh␈↓↓goal-plan recognition, and concealed goal-plan
␈↓ ↓H␈↓␈↓ ↓xinferential apparatus by using this ␈↓ εh␈↓↓recognition␈↓.
␈↓ ↓H␈↓␈↓ ↓xapparatus to indirectly simulate the
␈↓ ↓H␈↓␈↓ ↓xreasoning of other intelligent organisms ␈↓ εh␈↓⊗ Initial design of simple plan producer -
␈↓ ↓H␈↓␈↓ ↓x[Creary 1979]. This provides a natural and␈↓ εh␈↓␈↓ π_January 1982.
␈↓ ↓H␈↓␈↓ ↓xe␈↓↓␈↓β@␈↓↓␈↓icient approach to making realistic
␈↓ ↓H␈↓␈↓ ↓xinferences about the beliefs of others, and␈↓ εh␈↓⊗ Implementation and preliminary experiments
␈↓ ↓H␈↓␈↓ ↓xcan be generalized to handle desires, plans,␈↓ εh␈↓␈↓ π_with simple plan producer completed;
␈↓ ↓H␈↓␈↓ ↓xand intentions, as well. ␈↓ εh␈↓␈↓ π_initial design of simple plan recognizer
␈↓ εh␈↓␈↓ π_begun - April 1982.
␈↓ ↓H␈↓The next step in our design process will be to
␈↓ ↓H␈↓integrate the ideas from Creary's design studies␈↓ εh␈↓⊗ Implementation and preliminary experimetns
␈↓ ↓H␈↓of the advice taker with the ideas from ␈↓ εh␈↓␈↓ π_with simple plan recognizer underway -
␈↓ ↓H␈↓Gabriel's thesis, in order to arrive at a detailed␈↓ εh␈↓␈↓ π_June 1981.
␈↓ ↓H␈↓initial design for the problem solver.
␈↓ εh␈↓⊗ Re␈↓↓␈↓βC␈↓↓␈↓nement of simple plan recognizer and
␈↓ ↓H␈↓α␈↓ αsGoals and Milestones ␈↓ εh␈↓␈↓ π_design of goal-plan recognizer additions
␈↓ εh␈↓␈↓ π_begun - September 1982.
␈↓ ↓H␈↓The initial problem solving task will be the
␈↓ ↓H␈↓Airport Problem described in [McCarthy 1959].␈↓ εh␈↓⊗ Implementation and preliminary experiments
␈↓ ↓H␈↓Further experimentation will proceed with ␈↓ εh␈↓␈↓ π_with goal-plan recognizer completed -
␈↓ ↓H␈↓embellishments and complications of that ␈↓ εh␈↓␈↓ π_January 1982
␈↓ ↓H␈↓situation. In particular, further travel planning
␈↓ ↓H␈↓techniques will be added to the initial system␈↓ εh␈↓⊗ Re␈↓↓␈↓βC␈↓↓␈↓nement of goal-plan recognizer and
␈↓ ↓H␈↓through the means of advice taking, and ␈↓ εh␈↓␈↓ π_design of concealed goal-plan recognizer
␈↓ ↓H␈↓additional problems involving travel will be␈↓ εh␈↓␈↓ π_additions begun - March 1982.
␈↓ ↓H␈↓presented to it. At this point, the program will
␈↓ ↓H␈↓be capable of ␈↓↓simple plan production␈↓: the ␈↓ εh␈↓⊗ Concealed goal-plan recognizer completed
␈↓ ↓H␈↓construction of a travel plan, given a goal and␈↓ εh␈↓␈↓ π_October 1983
␈↓ ↓H␈↓suitable travel facts.
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ =15
␈↓ ↓H␈↓α␈↓ αλ␈↓ α 1.4.4 Architecture for Reasoning ␈↓ εh␈↓α␈↓ π(␈↓ π'1.4.5 Formalization of Mathematical
␈↓ ↓H␈↓ α␈␈↓α␈↓ αHPrograms ␈↓ εh␈↓ λ→␈↓α␈↓ πhReasoning
␈↓ ↓H␈↓Jon Doyle is engaged in the development of a␈↓ εh␈↓ Ketonen has been working on
␈↓ ↓H␈↓comprehensive architecture for reasoning ␈↓ εh␈↓formalization of mathematical reasoning. The
␈↓ ↓H␈↓programs. This architecture is based on the␈↓ εh␈↓emphasis has been on creating a system and a
␈↓ ↓H␈↓use of ␈↓ εh␈↓language which would allow the expression and
␈↓ εh␈↓veri␈↓↓␈↓βC␈↓↓␈↓cation of mathematical facts in a direct
␈↓ ↓H␈↓␈↓ ↓h1. multiple logical theories (extending those␈↓ εh␈↓and natural way. The approach taken has been
␈↓ ↓H␈↓␈↓ α_of Weyhrauch [1980]) and non- ␈↓ εh␈↓quite successful: Ketonen has been able to
␈↓ ↓H␈↓␈↓ α_monotonic inference records (as studied ␈↓ εh␈↓produce an elegant and eminently readable
␈↓ ↓H␈↓␈↓ α_in [Doyle 1979] and [McDermott and ␈↓ εh␈↓proof of Ramsey's theorem in under 100 lines.
␈↓ ↓H␈↓␈↓ α_Doyle 1980]) for memory representation,
␈↓ ↓H␈↓␈↓ ↓h2. explicit statements of mental attitudes and␈↓ εh␈↓ Ramsey's theorem has been used as a
␈↓ ↓H␈↓␈↓ α_their relations to the global mental state␈↓ εh␈↓benchmark to test the power of proof checking
␈↓ ↓H␈↓␈↓ α_(extending the proposals of [de Kleer, et ␈↓ εh␈↓systems: The previous known shortest
␈↓ ↓H␈↓␈↓ α_al. 1977]), ␈↓ εh␈↓computer-checked proof is due to Bulnes who
␈↓ ↓H␈↓␈↓ ↓h3. deliberate actions, both mental and extra-␈↓ εh␈↓proved it in about 400 lines.
␈↓ ↓H␈↓␈↓ α_mental, based on those attitudes
␈↓ ↓H␈↓␈↓ α_(extending [McDermott 1978]), and ␈↓ εh␈↓ The above result is important in that it
␈↓ ↓H␈↓␈↓ ↓h4. a deliberate, reasoned decision-making ␈↓ εh␈↓indicates that mathematical proofs previously
␈↓ ↓H␈↓␈↓ α_process, called reasoned deliberation, ␈↓ εh␈↓thought to be too complex for mechanical
␈↓ ↓H␈↓␈↓ α_which plans decision-making steps and ␈↓ εh␈↓veri␈↓↓␈↓βC␈↓↓␈↓cation are now within the reach of
␈↓ ↓H␈↓␈↓ α_uses non-monotonic inference records to ␈↓ εh␈↓su␈↓↓␈↓β@␈↓↓␈↓iciently powerful proof checking systems. In
␈↓ ↓H␈↓␈↓ α_conduct arguments about what to do. ␈↓ εh␈↓particular, Ketonen intends to apply the
␈↓ εh␈↓techniques that he has developed to verifying
␈↓ ↓H␈↓See the attached paper [Doyle 1981a] for a␈↓ εh␈↓the correctness of the various parsing
␈↓ ↓H␈↓more detailed overview of these techniques.␈↓ εh␈↓algorithms that are currently in fashion. These
␈↓ εh␈↓types of results are, of course, of great interest
␈↓ ↓H␈↓ The primary reference for this work is␈↓ εh␈↓in the ␈↓↓␈↓βC␈↓↓␈↓eld of compiler design.
␈↓ ↓H␈↓[Doyle 1980], but Doyle has recently completed
␈↓ ↓H␈↓drafts of two new papers: [Doyle 1981a], ␈↓ εh␈↓ Ketonen's approach is based on simple,
␈↓ ↓H␈↓submitted to IJCAI-81, and [Doyle 1981b]. ␈↓ εh␈↓yet powerful, proof construction primitives that
␈↓ ↓H␈↓Drafts of three other papers are in preparation␈↓ εh␈↓allow several ``proof modules'' to coexist
␈↓ ↓H␈↓[Doyle 1981c] [Doyle 1981d] [de Kleer and ␈↓ εh␈↓simultaneously in core and permit arbitrary
␈↓ ↓H␈↓Doyle 1981]. ␈↓ εh␈↓linkages between such modules. The use of
␈↓ εh␈↓these primitives can be programmed in LISP if
␈↓ ↓H␈↓ The goal of this work is the further␈↓ εh␈↓one so desires.
␈↓ ↓H␈↓development of these theories of memory,
␈↓ ↓H␈↓reasoning, action, and decision-making, towards␈↓ εh␈↓ One of Ketonen's techniques is a new
␈↓ ↓H␈↓the end of eventual implementation. ␈↓ εh␈↓type of a decision procedure used to verify
␈↓ εh␈↓simple facts in typed predicate calculus. It was
␈↓ ↓H␈↓ The milestones of this e␈↓↓␈↓β@␈↓↓␈↓ort are the␈↓ εh␈↓found during Ketonen's work on fragments of
␈↓ ↓H␈↓completions of several papers in progress ␈↓ εh␈↓predicate calculus admitting fast decision
␈↓ ↓H␈↓explaining in detail the improved theories and␈↓ εh␈↓procedures. Predicate logic has been
␈↓ ↓H␈↓their relations to other AI theories and ␈↓ εh␈↓traditionally viewed as the place to formalize
␈↓ ↓H␈↓techniques. Serious implementation of these␈↓ εh␈↓the notion of a ``logical inference''. Intuitively it
␈↓ ↓H␈↓ideas may have to be postponed pending the␈↓ εh␈↓is clear that any ``trivial'' inference should be
␈↓ ↓H␈↓availability of suitable computational facilities,␈↓ εh␈↓easily formalizable and decidable in predicate
␈↓ ↓H␈↓although preliminary studies are foreseen.␈↓ εh␈↓logic. As is well known, the full system of
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ >16
␈↓ ↓H␈↓predicate calculus is not decidable; thus one is␈↓ εh␈↓α␈↓ π(␈↓ π⊗1.4.6 Formal Systems for Computation
␈↓ ↓H␈↓led to study suitable fragments of predicate␈↓ εh␈↓ λ'␈↓α␈↓ πhTheories
␈↓ ↓H␈↓logic. Ketonen has isolated a fragment that
␈↓ ↓H␈↓seems particularly promising: In some intuitive␈↓ εh␈↓Carolyn Talcott is studying formal systems for
␈↓ ↓H␈↓sense it captures the notion of a ``direct''␈↓ εh␈↓representing structures, processes, and reasoning
␈↓ ↓H␈↓inference. The corresponding decision ␈↓ εh␈↓related to computation. The goal is to develop
␈↓ ↓H␈↓procedure works in exponential time and is␈↓ εh␈↓a formal system in which the commonly
␈↓ ↓H␈↓tailored to situations that occur naturally in␈↓ εh␈↓encountered concepts and principles can be
␈↓ ↓H␈↓actual mathematical practice. This work will be␈↓ εh␈↓expressed naturally. To begin with attention
␈↓ ↓H␈↓described in detail in a forthcoming paper by␈↓ εh␈↓will be focused on a LISP-like language.
␈↓ ↓H␈↓Ketonen and Weyhrauch. Ketonen intends to␈↓ εh␈↓Formalization of properties of computations
␈↓ ↓H␈↓continue his work on algorithms for typed ␈↓ εh␈↓and principles for veri␈↓↓␈↓βC␈↓↓␈↓cation of programs in
␈↓ ↓H␈↓predicate calculus - partial higher order ␈↓ εh␈↓the full language will demonstrate that this goal
␈↓ ↓H␈↓uni␈↓↓␈↓βC␈↓↓␈↓cation algorithms seem to be of particular␈↓ εh␈↓is a reaonable one.
␈↓ ↓H␈↓interest in this regard. Another advantage of
␈↓ ↓H␈↓cleanly presented ``modular'' proofs is their easy␈↓ εh␈↓α␈↓ λJApplications
␈↓ ↓H␈↓availability for computational purposes: Thus
␈↓ ↓H␈↓one can use the well known techniques of proof␈↓ εh␈↓Although the initial work will be abstract and
␈↓ ↓H␈↓normalization to extract computational ␈↓ εh␈↓technical, there are many practical applications.
␈↓ ↓H␈↓information from the proofs in question. ␈↓ εh␈↓Some of these are summarized below along
␈↓ εh␈↓with some important extensions.
␈↓ ↓H␈↓ Ketonen intends to apply these
␈↓ ↓H␈↓techniques to study variants of Ramsey's ␈↓ εh␈↓⊗ Mechanization of the system via
␈↓ ↓H␈↓theorem and to the question of computing ␈↓ εh␈↓formalization of metatheory and model theory.
␈↓ ↓H␈↓feasible bounds for the numbers occurring in␈↓ εh␈↓The intended model of the system will be
␈↓ ↓H␈↓Van der Waerden's theorem on arithmetic ␈↓ εh␈↓essential the data structures and programs for
␈↓ ↓H␈↓progressions. Once developed, these techniques␈↓ εh␈↓LISP like language. The structures for
␈↓ ↓H␈↓can be used to study program and proof ␈↓ εh␈↓representing the mechanizable aspects of the
␈↓ ↓H␈↓transformations in general. ␈↓ εh␈↓metatheory can be naturally encoded in the
␈↓ εh␈↓intended model.
␈↓ ↓H␈↓During the next two years Ketonen plans to:
␈↓ εh␈↓⊗ Proving properties of `real' LISP programs.
␈↓ ↓H␈↓␈↓ ↓h1. apply the techniques for proof checking␈↓ εh␈↓We will be able to treat programs that contain
␈↓ ↓H␈↓␈↓ α_that he has developed to verifying the ␈↓ εh␈↓arbitrary assignments, non-local control such as
␈↓ ↓H␈↓␈↓ α_correctness of the various parsing ␈↓ εh␈↓CATCH and THROW, as well as programs
␈↓ ↓H␈↓␈↓ α_algorithms that are currently in fashion. ␈↓ εh␈↓containing MACROs.
␈↓ ↓H␈↓␈↓ ↓h2. develop more powerful proof manipulation
␈↓ ↓H␈↓␈↓ α_techniques in order to study ␈↓ εh␈↓⊗ Mechanical veri␈↓↓␈↓βC␈↓↓␈↓cation of proofs. Natural
␈↓ ↓H␈↓␈↓ α_transformations of programs and proofs. ␈↓ εh␈↓representation of proofs will facilitate the
␈↓ ↓H␈↓␈↓ α_This methodology will then be used to ␈↓ εh␈↓interaction between the user and the proof
␈↓ ↓H␈↓␈↓ α_extract computational information out of ␈↓ εh␈↓checker. As in the FOL formalism
␈↓ ↓H␈↓␈↓ α_correctness proofs of programs and other ␈↓ εh␈↓[Weyhrauch 1977] having models, theories and
␈↓ ↓H␈↓␈↓ α_mathematical facts. ␈↓ εh␈↓metatheories available will facilitate
␈↓ ↓H␈↓␈↓ ↓h3. continue his study of algorithms for typed␈↓ εh␈↓development of proof schemes and
␈↓ ↓H␈↓␈↓ α_predicate calculus with special emphasis ␈↓ εh␈↓incorporating them as derived rules. For
␈↓ ↓H␈↓␈↓ α_on partial higher order uni␈↓↓␈↓βC␈↓↓␈↓cation ␈↓ εh␈↓example the [Boyer Moore 1979] principles of
␈↓ ↓H␈↓␈↓ α_algorithms. ␈↓ εh␈↓induction and recursion can be formulated and
␈↓ εh␈↓used. Also heuristics for manipulation of terms,
␈↓ εh␈↓formulae and proofs can be formulated and
␈↓ εh␈↓applied to make the computer a more
␈↓ εh␈↓`intelligent' assistant.
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ >17
␈↓ ↓H␈↓⊗ Abstract data structures (domains and ␈↓ εh␈↓will extend naturally to more the more complex
␈↓ ↓H␈↓operations) can be formulated in a natural␈↓ εh␈↓situations. The results are in general uniformly
␈↓ ↓H␈↓manner within the proposed system. Thus it␈↓ εh␈↓parameterized by the computation domain (the
␈↓ ↓H␈↓can be used as a framework for understanding␈↓ εh␈↓collection of data and operations taken to be
␈↓ ↓H␈↓data abstraction, and in particular for ␈↓ εh␈↓primitive).
␈↓ ↓H␈↓analyzing the notion of parameterized data type
␈↓ ↓H␈↓which has been the subject of recent ␈↓ εh␈↓Two notions of computation are distinguished,
␈↓ ↓H␈↓investigation from several points of view. See␈↓ εh␈↓which are called respectively `computation over
␈↓ ↓H␈↓for example [Thatcher, Wagner and Wright ␈↓ εh␈↓a data structure' and `computation over a
␈↓ ↓H␈↓1979] and [Cartwright 1980]. ␈↓ εh␈↓memory structure'. In the former, the primitive
␈↓ εh␈↓operations construct and examine data. (e.g in
␈↓ ↓H␈↓⊗ Formalization of the notion of a computation␈↓ εh␈↓pure LISP we have CAR, CDR, CONS,
␈↓ ↓H␈↓system = computation theory + implementation␈↓ εh␈↓EQUAL, ATOM) In the latter additional
␈↓ ↓H␈↓(model). Here we move from the static aspects␈↓ εh␈↓destructive primitive operations are allowed.
␈↓ ↓H␈↓of computation to the dynamic aspects of ␈↓ εh␈↓(e.g. RPLACs, array assignments, etc.) The
␈↓ ↓H␈↓interactive systems. An interactive and ␈↓ εh␈↓same basic language serves to de␈↓↓␈↓βC␈↓↓␈↓ne either form
␈↓ ↓H␈↓dynamically changing system is explained in␈↓ εh␈↓of computation. In either case computations
␈↓ ↓H␈↓terms of a theory, model and interpretation␈↓ εh␈↓de␈↓↓␈↓βC␈↓↓␈↓ned by natural syntactic subclasses of the
␈↓ ↓H␈↓(dynamically) connecting the two. ␈↓ εh␈↓languange are considered. These include pure
␈↓ εh␈↓recursive (no loops or assignments), iterative
␈↓ ↓H␈↓⊗ Formalization of the dynamic aspects ␈↓ εh␈↓(loops with assignment limited to local context),
␈↓ ↓H␈↓provides a framework for talking about ␈↓ εh␈↓mixed iterative and recursive, addition of
␈↓ ↓H␈↓activities such as declarations and de␈↓↓␈↓βC␈↓↓␈↓nitions,␈↓ εh␈↓unlimited assignment and non-local control
␈↓ ↓H␈↓DEBUGGING, for treating ERROR ␈↓ εh␈↓capabilities. Computations of either form
␈↓ ↓H␈↓conditions, and distinguishing kinds of ␈↓ εh␈↓de␈↓↓␈↓βC␈↓↓␈↓ned by an abstract machine (a la LAP) are
␈↓ ↓H␈↓unde␈↓↓␈↓βC␈↓↓␈↓nedness ␈↓↓␈↓βE␈↓↓␈↓ abnormal termination versus␈↓ εh␈↓also treated.
␈↓ ↓H␈↓non-termination.
␈↓ εh␈↓2. Veri␈↓↓␈↓βC␈↓↓␈↓cation technology ␈↓↓␈↓βE␈↓↓␈↓ partial correctness,
␈↓ ↓H␈↓α␈↓ αYWhat is to be formalized ␈↓ εh␈↓total correctness, termination. Many
␈↓ εh␈↓methodologies for veri␈↓↓␈↓βC␈↓↓␈↓cation of particular
␈↓ ↓H␈↓In order to motivate the criteria given below␈↓ εh␈↓classes of programs have been developed.
␈↓ ↓H␈↓for a suitable formal system for theories of␈↓ εh␈↓Some of the major ones include invariant
␈↓ ↓H␈↓computation we describe some of the main ␈↓ εh␈↓assertions, intermittent assertions, and subgoal
␈↓ ↓H␈↓ideas to be formalized. ␈↓ εh␈↓assertions for ␈↓↓␈↓βD␈↓↓␈↓ow chart type programs, subgoal
␈↓ εh␈↓induction, Scott (computation) induction, and
␈↓ ↓H␈↓1. Levels of computation (a la LISP) and ␈↓ εh␈↓McCarthy-Cartwright methods for proving
␈↓ ↓H␈↓interconnections. ␈↓ εh␈↓properties of recursive programs. The
␈↓ εh␈↓principles can be formulated to apply to the
␈↓ ↓H␈↓Talcott has been working on methods for ␈↓ εh␈↓appropriate subclass of computations from (1)
␈↓ ↓H␈↓formulating in a uniform and simple manner␈↓ εh␈↓and thus be applied and understood in a single
␈↓ ↓H␈↓the computations de␈↓↓␈↓βC␈↓↓␈↓ned by various classes of␈↓ εh␈↓context.
␈↓ ↓H␈↓programs. The `universe' is taken to be
␈↓ ↓H␈↓programs in a LISP-like language where ␈↓ εh␈↓3. Computations and programs as data. Here
␈↓ ↓H␈↓applicative, imperative,iterative, recursive and␈↓ εh␈↓we include such standard ideas as analysis of
␈↓ ↓H␈↓many other styles of programming are possible.␈↓ εh␈↓the computation de␈↓↓␈↓βC␈↓↓␈↓ned by a program and
␈↓ ↓H␈↓The idea is to de␈↓↓␈↓βC␈↓↓␈↓ne natural subclasses and␈↓ εh␈↓operations on programs such as compilation
␈↓ ↓H␈↓formulate natural embeddings among the ␈↓ εh␈↓and optimization. In addition there is the
␈↓ ↓H␈↓classes where appropriate. Thus reasoning and␈↓ εh␈↓notion of derived program developed by
␈↓ ↓H␈↓speci␈↓↓␈↓βC␈↓↓␈↓cation of properties can be carried out at␈↓ εh␈↓McCarthy. Derived programs compute
␈↓ ↓H␈↓an appropriate level of detail and the results␈↓ εh␈↓properties of the original program. Thus
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ =18
␈↓ ↓H␈↓various complexity measures (depth of ␈↓ εh␈↓and application) iteration (corresponding to
␈↓ ↓H␈↓recursion, number of CONSes, number of ␈↓ εh␈↓loop programs) and recursion. For major
␈↓ ↓H␈↓subroutine calls) can be expressed via derived␈↓ εh␈↓classes of programs, the function computed can
␈↓ ↓H␈↓programs. Also structures representing traces␈↓ εh␈↓be expressed naturally as a function of the
␈↓ ↓H␈↓or complete computation trees can be computed␈↓ εh␈↓system.
␈↓ ↓H␈↓by derived programs. There are general
␈↓ ↓H␈↓methods for deriving derived programs. ␈↓ εh␈↓2. A notion of set or class is needed. These
␈↓ ↓H␈↓Formalization of these methods and of the ␈↓ εh␈↓should be closed under such operations
␈↓ ↓H␈↓computation de␈↓↓␈↓βC␈↓↓␈↓ned by programs will provide␈↓ εh␈↓(boolean operations, cartesian product, partial
␈↓ ↓H␈↓means for proving that the derived programs␈↓ εh␈↓function spaces) . Limited principles of
␈↓ ↓H␈↓are `correct'. ␈↓ εh␈↓inductive de␈↓↓␈↓βC␈↓↓␈↓nition together with the
␈↓ εh␈↓corresponding principles for proof by induction
␈↓ ↓H␈↓4. Abstract Data Types. An important ␈↓ εh␈↓are also needed.
␈↓ ↓H␈↓technology for programming is the de␈↓↓␈↓βC␈↓↓␈↓nition of
␈↓ ↓H␈↓data types. This includes de␈↓↓␈↓βC␈↓↓␈↓nition of the␈↓ εh␈↓3. The system will be `parameterized' by the
␈↓ ↓H␈↓domain and primitive operations. There are␈↓ εh␈↓intended computation domain (the primitive
␈↓ ↓H␈↓various approaches specifying the means of␈↓ εh␈↓data types and operations). This re␈↓↓␈↓βD␈↓↓␈↓ects the
␈↓ ↓H␈↓de␈↓↓␈↓βC␈↓↓␈↓nition, one is the `constructive approach' of␈↓ εh␈↓principle of separation of control and data
␈↓ ↓H␈↓[Cartwright 1980]. Constructions should ␈↓ εh␈↓which is important for modularity and stability
␈↓ ↓H␈↓include cartesian product, combinatory ␈↓ εh␈↓of a computation system.
␈↓ ↓H␈↓operations, and restriction to decidable subsets.
␈↓ ↓H␈↓In addition means for de␈↓↓␈↓βC␈↓↓␈↓nition of functions␈↓ εh␈↓α␈↓ λ∪Goals and Milestones
␈↓ ↓H␈↓operating on the de␈↓↓␈↓βC␈↓↓␈↓ned data types and
␈↓ ↓H␈↓principles for proving properties are essential.␈↓ εh␈↓⊗ Specify in detail the ideas to be formalized,
␈↓ εh␈↓giving complete informal de␈↓↓␈↓βC␈↓↓␈↓nitions and proofs.
␈↓ ↓H␈↓α␈↓ α]Suitable formal systems
␈↓ εh␈↓⊗ De␈↓↓␈↓βC␈↓↓␈↓ne the basic formal system and enrich
␈↓ ↓H␈↓Talcott has been studying systems developed by␈↓ εh␈↓the collection of available formal notions via
␈↓ ↓H␈↓logicians for formalizing various kinds of␈↓ εh␈↓de␈↓↓␈↓βC␈↓↓␈↓nitions and derived principles so that the
␈↓ ↓H␈↓mathematics including constructive analysis,␈↓ εh␈↓work of formalization can be carried out in a
␈↓ ↓H␈↓constructive algebra, and logic. Many of the␈↓ εh␈↓direct and natural manner.
␈↓ ↓H␈↓results can be easily modi␈↓↓␈↓βC␈↓↓␈↓ed to apply to the
␈↓ ↓H␈↓project proposed. Of particular interest is the␈↓ εh␈↓⊗ Carry out detailed formaliztion for a variety
␈↓ ↓H␈↓work of Feferman[1978,1981] on formal systems␈↓ εh␈↓of examples.
␈↓ ↓H␈↓for constructive and explicit mathematics
␈↓ ↓H␈↓(analysis). Below are outlined some of the␈↓ εh␈↓⊗ Use formalization and properties of basic
␈↓ ↓H␈↓features essential to a system in which the ideas␈↓ εh␈↓formal system to explain relation among
␈↓ ↓H␈↓sketched above can be formalized naturally.␈↓ εh␈↓various veri␈↓↓␈↓βC␈↓↓␈↓cation technologies.
␈↓ ↓H␈↓1. Functions are part of the domain of ␈↓ εh␈↓⊗ Prove some non-trivial properties of
␈↓ ↓H␈↓discourse. Thus the notions of functions as␈↓ εh␈↓programs to demonstrate the expressive power
␈↓ ↓H␈↓arguments and functions as values are easily␈↓ εh␈↓of the formal system.
␈↓ ↓H␈↓represented. Classes of functions can be
␈↓ ↓H␈↓discussed. Principles for proving properties of
␈↓ ↓H␈↓special classes of functions, and procedures for
␈↓ ↓H␈↓manipulating or constructing special classes of
␈↓ ↓H␈↓functions can be formulated.
␈↓ ↓H␈↓Among the available means for de␈↓↓␈↓βC␈↓↓␈↓nition of
␈↓ ↓H␈↓functions will be explicit de␈↓↓␈↓βC␈↓↓␈↓nition (abstraction
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ >19
␈↓ ↓H␈↓α␈↓ α≠1.5 The Formal Reasoning Group ␈↓ εh␈↓groups. She is currently interested in the
␈↓ εh␈↓formalization of concepts and activities relating
␈↓ ↓H␈↓John McCarthy is Professor of Computer ␈↓ εh␈↓to computation, and the eventual application of
␈↓ ↓H␈↓Science and has worked in the area of formal␈↓ εh␈↓the results to representation of reasoning and
␈↓ ↓H␈↓reasoning applied to computer science and ␈↓ εh␈↓problem solving activities.
␈↓ ↓H␈↓arti␈↓↓␈↓βC␈↓↓␈↓cial intelligence since 1957. He is working
␈↓ ↓H␈↓on the logic of knowledge and belief, the ␈↓ εh␈↓α␈↓ λ=1.6 References
␈↓ ↓H␈↓circumscription mode of reasoning, formalizing
␈↓ ↓H␈↓properties of programs in ␈↓↓␈↓βC␈↓↓␈↓rst order logic and a␈↓ εh␈↓[Aiello 1980] Aiello, L., ␈↓αEvaluating functions
␈↓ ↓H␈↓general theory of patterns. ␈↓ εh␈↓α␈↓ π_de␈↓␈↓βc␈↓␈↓αned in ␈↓␈↓βc␈↓␈↓αrst-order logic␈↓ (submitted to
␈↓ εh␈↓␈↓ π_Logic Programming Conference, Budapest,
␈↓ ↓H␈↓Lewis Creary is Research Associate in ␈↓ εh␈↓␈↓ π_July 1980).
␈↓ ↓H␈↓Computer Science, received his doctorate from
␈↓ ↓H␈↓Princeton University in philosophy, and has␈↓ εh␈↓[Aiello and Weyhrauch 1980] Aiello, L. and
␈↓ ↓H␈↓been concerned with epistemology, semantics,␈↓ εh␈↓␈↓ π_Weyhrauch, R. W., ␈↓αUsing meta-theoretic
␈↓ ↓H␈↓logic, and a computational system for inductive␈↓ εh␈↓α␈↓ π_Reasoning to do Algebra␈↓, ␈↓↓Proc. Automatic
␈↓ ↓H␈↓inference. He is working on epistemological␈↓ εh␈↓↓␈↓ π_Deduction Conference␈↓, Les Arcs (France),
␈↓ ↓H␈↓problems of AI, representation of knowledge,␈↓ εh␈↓␈↓ π_July 8-11, 1980.
␈↓ ↓H␈↓and development of the new advice-taking
␈↓ ↓H␈↓ANALYST program. ␈↓ εh␈↓[Boyer, Moore 1979] Boyer, R.S., and Moore,
␈↓ εh␈↓␈↓ π_J.S., ␈↓αA Computational Logic␈↓ Academic
␈↓ ↓H␈↓Jon Doyle is a Research Associate in Computer␈↓ εh␈↓␈↓ π_Press, New York, 1979.
␈↓ ↓H␈↓Science. He received a doctorate from the
␈↓ ↓H␈↓Massachusetts Institute of Technology, and has␈↓ εh␈↓[Brooks 1980] Brooks, M., ␈↓αDetermining
␈↓ ↓H␈↓studied inference records, non-monotonic logics,␈↓ εh␈↓α␈↓ π_Correctness by Testing␈↓, Stanford AI Memo
␈↓ ↓H␈↓and architectures for reasoning programs. He␈↓ εh␈↓␈↓ π_Stanford AI Memo AIM-336 (May 1980).
␈↓ ↓H␈↓is developing theories and techniques for
␈↓ ↓H␈↓memory representation, mental attitudes, action-␈↓ εh␈↓[Bulnes-Rozas 1979] Bulnes-Rozas, J. B.,
␈↓ ↓H␈↓taking, decision-making, and learning. ␈↓ εh␈↓␈↓ π_␈↓αGOAL: A Goal Oriented Command
␈↓ εh␈↓α␈↓ π_Language for Interactive Proof
␈↓ ↓H␈↓Richard Gabriel is Research Associate in ␈↓ εh␈↓α␈↓ π_Constructions␈↓ Stanford AI Memo Stanford
␈↓ ↓H␈↓Computer Science, has a Ph.D. from Stanford␈↓ εh␈↓␈↓ π_AI Memo AIM-328, (June 1979).
␈↓ ↓H␈↓in computer science, and has been active in the
␈↓ ↓H␈↓␈↓↓␈↓βC␈↓↓␈↓elds of computer vision, natural language␈↓ εh␈↓[Cartwright 1980] Cartwright, R., ␈↓αA
␈↓ ↓H␈↓understanding, knowledge representation, ␈↓ εh␈↓α␈↓ π_Constructive Alternative to Axiomatic
␈↓ ↓H␈↓programming environments, programming ␈↓ εh␈↓α␈↓ π_Data Type De␈↓␈↓βc␈↓␈↓αnitions␈↓, Proceedings LISP
␈↓ ↓H␈↓language development, natural language ␈↓ εh␈↓␈↓ π_Conference, Stanford (1980).
␈↓ ↓H␈↓generation, and organizations for very large
␈↓ ↓H␈↓intelligent programs. He is working on the␈↓ εh␈↓[Cartwright and McCarthy 1979] Cartwright,
␈↓ ↓H␈↓design and implementation of advice takers.␈↓ εh␈↓␈↓ π_R. and McCarthy, J., ␈↓αRecursive Programs
␈↓ εh␈↓α␈↓ π_as Functions in a First Order Theory␈↓,
␈↓ ↓H␈↓Jussi Ketonen is a Research Associate in ␈↓ εh␈↓␈↓ π_Stanford AI Memo Stanford AI Memo
␈↓ ↓H␈↓Computer Science. He recieved his Ph.D. from␈↓ εh␈↓␈↓ π_AIM-324, (March 1979).
␈↓ ↓H␈↓University of Wisconsin in mathematical logic .
␈↓ ↓H␈↓He is interested in the mechanizable aspects of␈↓ εh␈↓[Creary 1979] Creary, Lewis G., ␈↓αPropositional
␈↓ ↓H␈↓formal reasoning. ␈↓ εh␈↓α␈↓ π_Attitudes: Fregean Representation and
␈↓ εh␈↓α␈↓ π_Simulative Reasoning,␈↓ ␈↓↓Proceedings of the
␈↓ ↓H␈↓Carolyn Talcott has a Ph.D. in chemistry from␈↓ εh␈↓↓␈↓ π_Sixth International Joint Conference on
␈↓ ↓H␈↓UC Berkeley and has done research in ␈↓ εh␈↓↓␈↓ π_Arti␈↓␈↓βS␈↓␈↓↓cial Intelligence␈↓, Tokyo, Japan:
␈↓ ↓H␈↓theoretical chemistry and theory of ␈↓↓␈↓βC␈↓↓␈↓nite ␈↓ εh␈↓␈↓ π_August 1979, 176-181.
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ <20
␈↓ ↓H␈↓[Creary 1981a] ␈↓αCausal Explanation and the ␈↓ εh␈↓[Feferman 1979] Feferman, S., ␈↓αConstructive
␈↓ ↓H␈↓α␈↓ ↓xReality of Natural Component Forces,␈↓ ␈↓ εh␈↓α␈↓ π_Theories of Functions and Classes␈↓, in
␈↓ ↓H␈↓␈↓ ↓xforthcoming in ␈↓↓Paci␈↓␈↓βS␈↓␈↓↓c Philosophical ␈↓ εh␈↓␈↓ π_Bo␈↓α␈↓β@␈↓α␈↓a,M. vanDalen,D. McAloon,K.(eds.)
␈↓ ↓H␈↓↓␈↓ ↓xQuarterly␈↓ 62 (April, 1981). ␈↓ εh␈↓␈↓ π_␈↓↓Logic Colloquium 78: U of Mons, Belgium
␈↓ εh␈↓↓␈↓ π_(August 1978)␈↓ North-Holland (1979) pp.
␈↓ ↓H␈↓[Creary 1981b] ␈↓αOn the Epistemology of ␈↓ εh␈↓␈↓ π_159-224.
␈↓ ↓H␈↓α␈↓ ↓xCommonsense Factual Reasoning:
␈↓ ↓H␈↓α␈↓ ↓xToward an Improved Theoretical Basis for ␈↓ εh␈↓[Feferman 1981] Feferman, S., ␈↓αTheories of
␈↓ ↓H␈↓α␈↓ ↓xReasoning Programs.␈↓ (in ␈↓α␈↓βC␈↓α␈↓nal stage of ␈↓ εh␈↓α␈↓ π_Variable Finite Type␈↓, (draft).
␈↓ ↓H␈↓␈↓ ↓xpreparation)
␈↓ εh␈↓[Gabriel 1980] Richard P. Gabriel, ␈↓↓An
␈↓ ↓H␈↓[Creary 1981c] ␈↓αOn the Nature of Causal ␈↓ εh␈↓↓␈↓ π_Organization for Programs in Fluid
␈↓ ↓H␈↓α␈↓ ↓xReasoning: The Frame and Quali␈↓␈↓βc␈↓␈↓αcation ␈↓ εh␈↓↓␈↓ π_Domains␈↓, Ph.D. Dissertation, Computer
␈↓ ↓H␈↓α␈↓ ↓xProblems.␈↓ (in preparation) ␈↓ εh␈↓␈↓ π_Science Department, Stanford University,
␈↓ εh␈↓␈↓ π_December 1980.
␈↓ ↓H␈↓[Creary 1981d] ␈↓αNeo-Fregean Foundations for
␈↓ ↓H␈↓α␈↓ ↓xAction Theory: Semantics for AI ␈↓ εh␈↓[Goad 1980a] Goad, C. A., ␈↓αProofs as
␈↓ ↓H␈↓α␈↓ ↓xRepresentations.␈↓ (in preparation) ␈↓ εh␈↓α␈↓ π_descriptions of computations␈↓, ␈↓↓Proc.
␈↓ εh␈↓↓␈↓ π_Automatic Deduction Conference␈↓, Les Arcs
␈↓ ↓H␈↓[de Kleer, Doyle, Steele, and Sussman 1977] de␈↓ εh␈↓␈↓ π_(France), July 8-11, 1980.
␈↓ ↓H␈↓␈↓ ↓xKleer, J., Doyle, J., Steele, G., and Sussman,
␈↓ ↓H␈↓␈↓ ↓xG., ␈↓αExplicit Control of Reasoning␈↓, MIT ␈↓ εh␈↓[Goad 1980b] Goad, C. A., ␈↓αComputational
␈↓ ↓H␈↓␈↓ ↓xAI Lab, Memo 427 (1977). ␈↓ εh␈↓α␈↓ π_Uses of the Manipulation of Formal
␈↓ εh␈↓α␈↓ π_Proofs␈↓, Stanford Computer Science
␈↓ ↓H␈↓[de Kleer and Doyle 1981] de Kleer, J., and␈↓ εh␈↓␈↓ π_Department Memo, STAN-CS-80-819
␈↓ ↓H␈↓␈↓ ↓xDoyle, J., ␈↓αSelf-interpretation and the ␈↓ εh␈↓␈↓ π_(1980).
␈↓ ↓H␈↓α␈↓ ↓xControl of Reasoning␈↓, (in preparation).
␈↓ εh␈↓[Hayes-Roth 1978] Hayes-Roth, Frederick, ␈↓αThe
␈↓ ↓H␈↓[Doyle 1979] Doyle, J., ␈↓αA Truth Maintenance␈↓ εh␈↓α␈↓ π_Role of Partial and Best Matches in
␈↓ ↓H␈↓α␈↓ ↓xSystem␈↓, Arti␈↓α␈↓βC␈↓α␈↓cial Intelligence 12, (1979), pp.␈↓ εh␈↓α␈↓ π_Knowledge Systems␈↓, in ␈↓↓Pattern-Directed
␈↓ ↓H␈↓␈↓ ↓x231-272. ␈↓ εh␈↓↓␈↓ π_Inference Systems␈↓, edited by D.A. Waterman
␈↓ εh␈↓␈↓ π_and Frederick Hayes-Roth, New York:
␈↓ ↓H␈↓[Doyle 1980] Doyle, J., ␈↓αA Model for ␈↓ εh␈↓␈↓ π_Academic Press, 1978.
␈↓ ↓H␈↓α␈↓ ↓xDeliberation, Action, and Introspection␈↓,
␈↓ ↓H␈↓␈↓ ↓xMIT AI Lab, TR-581, (1980). ␈↓ εh␈↓[Ketonen 1981] Ketonen, J., ␈↓αE␈↓␈↓β`␈↓␈↓αicient theorem
␈↓ εh␈↓α␈↓ π_proving in set theory␈↓, (To appear).
␈↓ ↓H␈↓[Doyle 1981a] Doyle, J., ␈↓αSketch of a Model for
␈↓ ↓H␈↓α␈↓ ↓xDeliberation, Action, and Introspection␈↓, ␈↓ εh␈↓[Ketonen 1981] Ketonen, J., ␈↓αOn a decidable
␈↓ ↓H␈↓␈↓ ↓x(draft, submitted to IJCAI-81). ␈↓ εh␈↓α␈↓ π_fragment of predicate calculus␈↓, (To
␈↓ εh␈↓␈↓ π_appear).
␈↓ ↓H␈↓[Doyle 1981b] Doyle, J., ␈↓αThree Short Essays on
␈↓ ↓H␈↓α␈↓ ↓xDecisions, Reasons, and Logics␈↓, (draft, ␈↓ εh␈↓[Ketonen and Weyhrauch 1981] Ketonen, J.,
␈↓ ↓H␈↓␈↓ ↓xStanford University memo). ␈↓ εh␈↓␈↓ π_and Weyhrauch, R. W., ␈↓αA semidecision
␈↓ εh␈↓α␈↓ π_procedure for predicate calculus␈↓, (To
␈↓ ↓H␈↓[Doyle 1981c] Doyle, J., ␈↓αA Theory of Memory␈↓,␈↓ εh␈↓␈↓ π_appear).
␈↓ ↓H␈↓␈↓ ↓x(in preparation).
␈↓ εh␈↓[Manna and Waldinger 1978] Manna, Z. and
␈↓ ↓H␈↓[Doyle 1981d] Doyle, J., ␈↓αSteps Towards ␈↓ εh␈↓␈↓ π_Waldinger, R., ␈↓αIs SOMETIME Sometimes
␈↓ ↓H␈↓α␈↓ ↓xArti␈↓␈↓βc␈↓␈↓αcial Intelligence␈↓, (in preparation). ␈↓ εh␈↓α␈↓ π_Better than ALWAYS? Intermittant
␈↓ εh␈↓α␈↓ π_Assertions in Proving Program
␈↓ εh␈↓α␈↓ π_Correctness␈↓, CACM, 21 (1978), pp. 159-172.
␈↓ ↓H␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence and Formal Reasoning␈↓ >21
␈↓ ↓H␈↓[McCarthy 1959] McCarthy, J., ␈↓αPrograms with␈↓ εh␈↓[Talcott 1981] Talcott, C., ␈↓αReasoning About
␈↓ ↓H␈↓α␈↓ ↓xCommon Sense␈↓, Proc. Int. Conf. on ␈↓ εh␈↓α␈↓ π_LISP: a Tutorial in Formalizing
␈↓ ↓H␈↓␈↓ ↓xMechanisation of Thought Processes, ␈↓ εh␈↓α␈↓ π_Properties of LISP Programs and Their
␈↓ ↓H␈↓␈↓ ↓xTeddington, England, National Physical ␈↓ εh␈↓α␈↓ π_Proofs.␈↓ Stanford AI Memo, forthcoming,
␈↓ ↓H␈↓␈↓ ↓xLaboratory, (1959). ␈↓ εh␈↓␈↓ π_(1981).
␈↓ ↓H␈↓[McCarthy and Hayes 1969] McCarthy, J. and␈↓ εh␈↓[Talcott and Weyhrauch 1981] Talcott, C. and
␈↓ ↓H␈↓␈↓ ↓xHayes, P., ␈↓αSome Philosophical Problems ␈↓ εh␈↓␈↓ π_Weyhrauch, R. W., ␈↓αThe Blind Robot
␈↓ ↓H␈↓α␈↓ ↓xfrom the Standpoint of Arti␈↓␈↓βc␈↓␈↓αcial ␈↓ εh␈↓α␈↓ π_Puzzle: A Paradigm for Representing and
␈↓ ↓H␈↓α␈↓ ↓xIntelligence␈↓, Stanford AI Memo AIM-73, ␈↓ εh␈↓α␈↓ π_Using Partial Knowldege␈↓, Stanford AI
␈↓ ↓H␈↓␈↓ ↓xNovember 1968; also in D. Michie (ed.), ␈↓ εh␈↓␈↓ π_Memo, forthcoming, (1981).
␈↓ ↓H␈↓␈↓ ↓x␈↓↓Machine Intelligence,␈↓ American Elsevier,
␈↓ ↓H␈↓␈↓ ↓xNew York, (1969). ␈↓ εh␈↓[Thatcher, Wagner and Wright 1979]
␈↓ εh␈↓␈↓ π_Thatcher, J. W., Wagner, E. G. and Wright,
␈↓ ↓H␈↓[McCarthy 1977] McCarthy, J., ␈↓ εh␈↓␈↓ π_J. B., ␈↓αData Type Speci␈↓␈↓βc␈↓␈↓αcation:
␈↓ ↓H␈↓␈↓ ↓x␈↓αEpistemological Problems of Arti␈↓␈↓βc␈↓␈↓αcial ␈↓ εh␈↓α␈↓ π_Parameterization and the Power of
␈↓ ↓H␈↓α␈↓ ↓xIntelligence␈↓, Proc. of the 5th International␈↓ εh␈↓α␈↓ π_Speci␈↓␈↓βc␈↓␈↓αcation Techniques␈↓, IBM Research
␈↓ ↓H␈↓␈↓ ↓xJoint Conference on Arti␈↓α␈↓βC␈↓α␈↓cial Intelligence,␈↓ εh␈↓␈↓ π_report RC-7757(1979).
␈↓ ↓H␈↓␈↓ ↓x(1977) (Invited Paper).
␈↓ εh␈↓[Weyhrauch 1977] Weyhrauch, R.W., ␈↓αA Users
␈↓ ↓H␈↓[McCarthy 1979] McCarthy, J., ␈↓αFirst Order ␈↓ εh␈↓α␈↓ π_Manual for FOL␈↓, Stanford AI Memo
␈↓ ↓H␈↓α␈↓ ↓xTheories of Individual Concepts and ␈↓ εh␈↓␈↓ π_Stanford AI Memo AIM-235.1, (July 1977).
␈↓ ↓H␈↓α␈↓ ↓xPropositions␈↓, in Michie, Donald (ed.)
␈↓ ↓H␈↓␈↓ ↓x␈↓↓Machine Intelligence 9␈↓, (University of ␈↓ εh␈↓[Wilkins 1979] Wilkins, D. E., ␈↓αUsing Patterns
␈↓ ↓H␈↓␈↓ ↓xEdinburgh Press, Edinburgh), Stanford AI ␈↓ εh␈↓α␈↓ π_and Plans to Solve Problems and Control
␈↓ ↓H␈↓␈↓ ↓xMemo Stanford AI Memo AIM-325 ␈↓ εh␈↓α␈↓ π_Search␈↓ Stanford AI Memo Stanford AI
␈↓ ↓H␈↓␈↓ ↓x(March 1979). ␈↓ εh␈↓␈↓ π_Memo AIM-329, (June 1979).
␈↓ ↓H␈↓[McCarthy 1980a] McCarthy, J.,
␈↓ ↓H␈↓␈↓ ↓x␈↓αCircumscription - A Form of Non-
␈↓ ↓H␈↓α␈↓ ↓xMonotonic Reasoning␈↓, ␈↓↓Arti␈↓␈↓βS␈↓␈↓↓cial
␈↓ ↓H␈↓↓␈↓ ↓xIntelligence␈↓, Volume 13, Numbers 1,2, April.
␈↓ ↓H␈↓␈↓ ↓xStanford AI Memo Stanford AI Memo
␈↓ ↓H␈↓␈↓ ↓xAIM-334 (February 1980).
␈↓ ↓H␈↓[McCarthy 1980b] McCarthy, J., ␈↓αThe Elephant
␈↓ ↓H␈↓α␈↓ ↓xLanguage for Representing Programs␈↓ (to
␈↓ ↓H␈↓␈↓ ↓xappear).
␈↓ ↓H␈↓[McCarthy and Talcott 1980] McCArthy, J.,
␈↓ ↓H␈↓␈↓ ↓xand Talcott, C., ␈↓↓LISP:Programming and
␈↓ ↓H␈↓↓␈↓ ↓xProving␈↓, (to appear, available as Stanford
␈↓ ↓H␈↓␈↓ ↓xCS206 Course Notes, Fall 1980)
␈↓ ↓H␈↓[McDermott 1978] McDermott, D., ␈↓αPlanning
␈↓ ↓H␈↓α␈↓ ↓xand Acting␈↓, Cognitive Science 2, (1978), pp.
␈↓ ↓H␈↓␈↓ ↓x71-109.
␈↓ ↓H␈↓[McDermott and Doyle 1980] McDermott, D.,
␈↓ ↓H␈↓␈↓ ↓xand Doyle, J., ␈↓αNon-monotonic Logic I␈↓,
␈↓ ↓H␈↓␈↓ ↓xArti␈↓α␈↓βC␈↓α␈↓cial Intelligence 13, (1980), pp. 41-72.